| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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{http://isa-afp.org/entries/Bertrands_Postulate.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Pratt_Certificate |
| Used by: | Dirichlet_L |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |