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 · 𝑁 ) ) )