Bertrand's postulate (Q7361411)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Bertrands_Postulate
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Bertrand's postulate |
AFP entry Bertrands_Postulate |
Statements
17 January 2017
0 references
Julian Biendarra
0 references
Manuel Eberl
0 references
Lawrence C. Paulson
0 references
Bertrand's postulate (English)
0 references
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.
0 references
