This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bpos

Description: Bertrand's postulate: there is a prime between N and 2 N for every positive integer N . This proof follows Erdős's method, for the most part, but with some refinements due to Shigenori Tochiori to save us some calculations of large primes. See http://en.wikipedia.org/wiki/Proof_of_Bertrand%27s_postulate for an overview of the proof strategy. This is Metamath 100 proof #98. (Contributed by Mario Carneiro, 14-Mar-2014)

Ref Expression
Assertion bpos ⊢ N ∈ ℕ → ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N

Proof

Step Hyp Ref Expression
1 bpos1 ⊢ N ∈ ℕ ∧ N ≤ 64 → ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N
2 eqid ⊢ n ∈ ℕ ⟼ 2 ⁢ x ∈ ℝ + ⟼ log ⁡ x x ⁡ n + 9 4 ⁢ x ∈ ℝ + ⟼ log ⁡ x x ⁡ n 2 + log ⁡ 2 2 ⁢ n = n ∈ ℕ ⟼ 2 ⁢ x ∈ ℝ + ⟼ log ⁡ x x ⁡ n + 9 4 ⁢ x ∈ ℝ + ⟼ log ⁡ x x ⁡ n 2 + log ⁡ 2 2 ⁢ n
3 eqid ⊢ x ∈ ℝ + ⟼ log ⁡ x x = x ∈ ℝ + ⟼ log ⁡ x x
4 simpll ⊢ N ∈ ℕ ∧ 64 < N ∧ ¬ ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N → N ∈ ℕ
5 simplr ⊢ N ∈ ℕ ∧ 64 < N ∧ ¬ ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N → 64 < N
6 simpr ⊢ N ∈ ℕ ∧ 64 < N ∧ ¬ ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N → ¬ ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N
7 2 3 4 5 6 bposlem9 ⊢ N ∈ ℕ ∧ 64 < N ∧ ¬ ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N → ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N
8 7 pm2.18da ⊢ N ∈ ℕ ∧ 64 < N → ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N
9 nnre ⊢ N ∈ ℕ → N ∈ ℝ
10 6nn0 ⊢ 6 ∈ ℕ 0
11 4nn0 ⊢ 4 ∈ ℕ 0
12 10 11 deccl ⊢ 64 ∈ ℕ 0
13 12 nn0rei ⊢ 64 ∈ ℝ
14 lelttric ⊢ N ∈ ℝ ∧ 64 ∈ ℝ → N ≤ 64 ∨ 64 < N
15 9 13 14 sylancl ⊢ N ∈ ℕ → N ≤ 64 ∨ 64 < N
16 1 8 15 mpjaodan ⊢ N ∈ ℕ → ∃ p ∈ ℙ N < p ∧ p ≤ 2 ⋅ N