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 ( 𝑁 ∈ ℕ → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 bpos1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 6 4 ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
2 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( √ ‘ 2 ) · ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) ) ‘ ( √ ‘ 𝑛 ) ) ) + ( ( 9 / 4 ) · ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) ) ‘ ( 𝑛 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( √ ‘ 2 ) · ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) ) ‘ ( √ ‘ 𝑛 ) ) ) + ( ( 9 / 4 ) · ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) ) ‘ ( 𝑛 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑛 ) ) ) ) )
3 eqid ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) )
4 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 6 4 < 𝑁 ) ∧ ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) → 𝑁 ∈ ℕ )
5 simplr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 6 4 < 𝑁 ) ∧ ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) → 6 4 < 𝑁 )
6 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 6 4 < 𝑁 ) ∧ ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
7 2 3 4 5 6 bposlem9 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 6 4 < 𝑁 ) ∧ ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
8 7 pm2.18da ⊢ ( ( 𝑁 ∈ ℕ ∧ 6 4 < 𝑁 ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
9 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
10 6nn0 ⊢ 6 ∈ ℕ0
11 4nn0 ⊢ 4 ∈ ℕ0
12 10 11 deccl ⊢ 6 4 ∈ ℕ0
13 12 nn0rei ⊢ 6 4 ∈ ℝ
14 lelttric ⊢ ( ( 𝑁 ∈ ℝ ∧ 6 4 ∈ ℝ ) → ( 𝑁 ≤ 6 4 ∨ 6 4 < 𝑁 ) )
15 9 13 14 sylancl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 6 4 ∨ 6 4 < 𝑁 ) )
16 1 8 15 mpjaodan ⊢ ( 𝑁 ∈ ℕ → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )