English
For every positive natural number n, there exists a prime p such that n < p ≤ 2n.
Русский
Для любого положительного натурального числа n существует простое p такое, что n < p ≤ 2n.
LaTeX
$$$\forall n \in \mathbb{N}_{>0}, \; \exists p \in \mathbb{N},\; p \text{ prime} \wedge n < p \wedge p \le 2n$$$
Lean4
/-- **Bertrand's Postulate**: For any positive natural number, there is a prime which is greater than
it, but no more than twice as large.
-/
theorem exists_prime_lt_and_le_two_mul (n : ℕ) (hn0 : n ≠ 0) : ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n := by
-- Split into cases whether `n` is large or small
rcases lt_or_ge 511 n with h | h
· exact exists_prime_lt_and_le_two_mul_eventually n h
replace h : n < 521 := h.trans_lt (by norm_num1)
revert h
open Lean Elab
Tactic in
run_tac
do
for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2]do
let i : Term := quote i
evalTactic <| ← `(tactic| refine exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) ?_)
exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩
