Theorems · Tour

What does Bertrand's postulate rest on?

For every positive n there is a prime between n and 2n. Mathlib proves it the way Erdős did: if no such prime existed, the central binomial coefficient (2n choose n) would be too small. Follow the chain from the theorem down to the definition of a prime.

Step 1 of 11 · depth 217 · cited by 0 · link
Nat.bertrand
The theorem: a prime p with n < p ≤ 2n exists for every positive n.
```
∀ (n : ℕ), n ≠ 0 → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
```
Alias of Nat.exists_prime_lt_and_le_two_mul.
Step 2 of 11 · depth 216 · cited by 1 · link
Nat.exists_prime_lt_and_le_two_mul
The working statement. Small n are checked by hand; large n go to the next step.
```
∀ (n : ℕ), n ≠ 0 → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
```
Bertrand's Postulate: For any positive natural number, there is a prime which is greater than it, but no more than twice as large.
Step 3 of 11 · depth 215 · cited by 1 · link
Nat.exists_prime_lt_and_le_two_mul_eventually
The case n ≥ 512, argued by contradiction from the two bounds that follow.
```
∀ (n : ℕ), 512 ≤ n → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
```
Proves that Bertrand's postulate holds for all sufficiently large n.
Step 4 of 11 · depth 104 · cited by 1 · link
centralBinom_le_of_no_bertrand_prime
If no prime lay in (n, 2n], the central binomial coefficient would be bounded above by a product that is too small.
```
∀ (n : ℕ),
  2 < n → (∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p) → n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
```
An upper bound on the central binomial coefficient used in the proof of Bertrand's postulate. The bound splits the prime factors of centralBinom n into those 1. At most sqrt (2 * n), which contribute at most 2 * n for each such prime. 2. Between sqrt (2 * n) and 2 * n / 3, which contribute at most 4^(2 * n / 3) in total. 3. Between 2 * n / 3 and n, which do not exist. 4. Between n and 2 * n, which would not exist in the case where Bertrand's postulate is false. 5. Above 2 * n, which do not exist.
Step 5 of 11 · depth 214 · cited by 1 · link
bertrand_main_inequality
The numerical inequality that makes the contradiction bite for n ≥ 512.
```
∀ {n : ℕ}, 512 ≤ n → n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
```
The inequality which contradicts Bertrand's postulate, for large enough n.
Step 6 of 11 · depth 40 · cited by 2 · link
Nat.four_pow_lt_mul_centralBinom
The lower bound: 4^n is less than n times the central binomial coefficient.
```
∀ (n : ℕ), 4 ≤ n → 4 ^ n < n * n.centralBinom
```
An exponential lower bound on the central binomial coefficient. This bound is of interest because it appears in [Tochiori's refinement of Erdős's proof of Bertrand's postulate](tochiori_bertrand).
Step 7 of 11 · depth 83 · cited by 0 · link
primorial_le_4_pow
The product of all primes up to n is at most 4^n, the upper-bound ingredient.
```
∀ (n : ℕ), primorial n ≤ 4 ^ n
```
Alias of primorial_le_four_pow.
Step 8 of 11 · depth 102 · cited by 1 · link
Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul
Primes between 2n/3 and n do not divide the central binomial coefficient at all.
```
∀ {p n : ℕ}, 2 < n → p ≤ n → 2 * n < 3 * p → n.centralBinom.factorization p = 0
```
Primes greater than about 2 * n / 3 and less than n do not appear in the factorization of centralBinom n.
Step 9 of 11 · depth 10 · cited by 24 · link
Nat.centralBinom
The central binomial coefficient, the object the whole argument is about.
```
ℕ → ℕ
```
The central binomial coefficient, Nat.choose (2 * n) n.
Step 10 of 11 · depth 86 · cited by 215 · link
Nat.factorization
The exponent of each prime in a number, the bookkeeping tool of the proof.
```
ℕ → ℕ →₀ ℕ
```
n.factorization is the finitely supported function ℕ →₀ ℕ mapping each prime factor of n to its multiplicity in n.
Step 11 of 11 · depth 19 · cited by 2,059 · link
Nat.Prime
What a prime is. Below this there are only the natural numbers and the axioms.
```
ℕ → Prop
```
Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. The theorem Nat.prime_def witnesses this description of a prime number.

Below the last step lie the natural numbers, propositional logic, and Lean's axioms. Open any step to keep descending on your own.