English
Bertrand's postulate holds for all sufficiently large natural numbers: there exists a prime p with n < p ≤ 2n whenever n is large enough (e.g., n ≥ 512).
Русский
Постулат Бертанда выполняется для всех достаточно больших натуральных чисел: существует простое p такое, что n < p ≤ 2n при sufficiently large n (например, n ≥ 512).
LaTeX
$$$\forall n \in \mathbb{N},\; 512 \le n \Rightarrow \exists p \in \mathbb{N},\; p \text{ prime} \land n < p \land p \le 2n.$$$
Lean4
/-- Proves that **Bertrand's postulate** holds for all sufficiently large `n`.
-/
theorem exists_prime_lt_and_le_two_mul_eventually (n : ℕ) (n_large : 512 ≤ n) : ∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n :=
by
-- Assume there is no prime in the range.
by_contra no_prime
have H1 : n * (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n := bertrand_main_inequality n_large
have H2 : 4 ^ n < n * n.centralBinom := Nat.four_pow_lt_mul_centralBinom n (le_trans (by norm_num1) n_large)
have H3 : n.centralBinom ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) :=
centralBinom_le_of_no_bertrand_prime n (lt_of_lt_of_le (by norm_num1) n_large) no_prime
rw [mul_assoc] at H1; exact not_le.2 H2 ((mul_le_mul_left' H3 n).trans H1)
