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⁡xx⁡n+94⁢x∈ℝ+⟼log⁡xx⁡n2+log⁡22⁢n=n∈ℕ⟼2⁢x∈ℝ+⟼log⁡xx⁡n+94⁢x∈ℝ+⟼log⁡xx⁡n2+log⁡22⁢n
3 eqid ⊢x∈ℝ+⟼log⁡xx=x∈ℝ+⟼log⁡xx
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