# Bertrand's postulate

 Title: Bertrand's postulate Authors: Julian Biendarra and Manuel Eberl Contributor: Lawrence C. Paulson Submission date: 2017-01-17 Abstract: Bertrand's postulate is an early result on the distribution of prime numbers: For every positive integer n, there exists a prime number that lies strictly between n and 2n. The proof is ported from John Harrison's formalisation in HOL Light. It proceeds by first showing that the property is true for all n greater than or equal to 600 and then showing that it also holds for all n below 600 by case distinction. BibTeX: @article{Bertrands_Postulate-AFP, author = {Julian Biendarra and Manuel Eberl}, title = {Bertrand's postulate}, journal = {Archive of Formal Proofs}, month = jan, year = 2017, note = {\url{https://isa-afp.org/entries/Bertrands_Postulate.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Pratt_Certificate Used by: Dirichlet_L, Frequency_Moments