Metamath Proof Explorer


Theorem bpos1

Description: Bertrand's postulate, checked numerically for N <_ 6 4 , using the prime sequence 2 , 3 , 5 , 7 , 1 3 , 2 3 , 4 3 , 8 3 . (Contributed by Mario Carneiro, 12-Mar-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Assertion bpos1 ( ( 𝑁 ∈ ℕ ∧ 𝑁 6 4 ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elnnuz ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ ‘ 1 ) )
2 ax-1 ( ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
3 6nn0 6 ∈ ℕ0
4 4nn0 4 ∈ ℕ0
5 3 4 deccl 6 4 ∈ ℕ0
6 5 nn0rei 6 4 ∈ ℝ
7 6 a1i ( 𝑁 ∈ ( ℤ 8 3 ) → 6 4 ∈ ℝ )
8 8nn0 8 ∈ ℕ0
9 3nn0 3 ∈ ℕ0
10 8 9 deccl 8 3 ∈ ℕ0
11 10 nn0rei 8 3 ∈ ℝ
12 11 a1i ( 𝑁 ∈ ( ℤ 8 3 ) → 8 3 ∈ ℝ )
13 eluzelre ( 𝑁 ∈ ( ℤ 8 3 ) → 𝑁 ∈ ℝ )
14 4lt10 4 < 1 0
15 6lt8 6 < 8
16 3 8 4 9 14 15 decltc 6 4 < 8 3
17 16 a1i ( 𝑁 ∈ ( ℤ 8 3 ) → 6 4 < 8 3 )
18 eluzle ( 𝑁 ∈ ( ℤ 8 3 ) → 8 3 ≤ 𝑁 )
19 7 12 13 17 18 ltletrd ( 𝑁 ∈ ( ℤ 8 3 ) → 6 4 < 𝑁 )
20 ltnle ( ( 6 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 6 4 < 𝑁 ↔ ¬ 𝑁 6 4 ) )
21 6 13 20 sylancr ( 𝑁 ∈ ( ℤ 8 3 ) → ( 6 4 < 𝑁 ↔ ¬ 𝑁 6 4 ) )
22 19 21 mpbid ( 𝑁 ∈ ( ℤ 8 3 ) → ¬ 𝑁 6 4 )
23 22 pm2.21d ( 𝑁 ∈ ( ℤ 8 3 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
24 83prm 8 3 ∈ ℙ
25 4 9 deccl 4 3 ∈ ℕ0
26 2nn0 2 ∈ ℕ0
27 eqid 4 3 = 4 3
28 4t2e8 ( 4 · 2 ) = 8
29 3t2e6 ( 3 · 2 ) = 6
30 26 4 9 27 28 29 decmul1 ( 4 3 · 2 ) = 8 6
31 3lt10 3 < 1 0
32 4lt8 4 < 8
33 4 8 9 9 31 32 decltc 4 3 < 8 3
34 6nn 6 ∈ ℕ
35 3lt6 3 < 6
36 8 9 34 35 declt 8 3 < 8 6
37 36 orci ( 8 3 < 8 6 ∨ 8 3 = 8 6 )
38 2 23 24 25 30 33 37 bpos1lem ( 𝑁 ∈ ( ℤ 4 3 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
39 43prm 4 3 ∈ ℙ
40 26 9 deccl 2 3 ∈ ℕ0
41 eqid 2 3 = 2 3
42 2t2e4 ( 2 · 2 ) = 4
43 26 26 9 41 42 29 decmul1 ( 2 3 · 2 ) = 4 6
44 2lt4 2 < 4
45 26 4 9 9 31 44 decltc 2 3 < 4 3
46 4 9 34 35 declt 4 3 < 4 6
47 46 orci ( 4 3 < 4 6 ∨ 4 3 = 4 6 )
48 2 38 39 40 43 45 47 bpos1lem ( 𝑁 ∈ ( ℤ 2 3 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
49 23prm 2 3 ∈ ℙ
50 1nn0 1 ∈ ℕ0
51 50 9 deccl 1 3 ∈ ℕ0
52 eqid 1 3 = 1 3
53 2cn 2 ∈ ℂ
54 53 mulid2i ( 1 · 2 ) = 2
55 26 50 9 52 54 29 decmul1 ( 1 3 · 2 ) = 2 6
56 1lt2 1 < 2
57 50 26 9 9 31 56 decltc 1 3 < 2 3
58 26 9 34 35 declt 2 3 < 2 6
59 58 orci ( 2 3 < 2 6 ∨ 2 3 = 2 6 )
60 2 48 49 51 55 57 59 bpos1lem ( 𝑁 ∈ ( ℤ 1 3 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
61 13prm 1 3 ∈ ℙ
62 7nn0 7 ∈ ℕ0
63 7t2e14 ( 7 · 2 ) = 1 4
64 1nn 1 ∈ ℕ
65 7lt10 7 < 1 0
66 64 9 62 65 declti 7 < 1 3
67 4nn 4 ∈ ℕ
68 3lt4 3 < 4
69 50 9 67 68 declt 1 3 < 1 4
70 69 orci ( 1 3 < 1 4 ∨ 1 3 = 1 4 )
71 2 60 61 62 63 66 70 bpos1lem ( 𝑁 ∈ ( ℤ ‘ 7 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
72 7prm 7 ∈ ℙ
73 5nn0 5 ∈ ℕ0
74 5t2e10 ( 5 · 2 ) = 1 0
75 5lt7 5 < 7
76 65 orci ( 7 < 1 0 ∨ 7 = 1 0 )
77 2 71 72 73 74 75 76 bpos1lem ( 𝑁 ∈ ( ℤ ‘ 5 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
78 5prm 5 ∈ ℙ
79 3lt5 3 < 5
80 5lt6 5 < 6
81 80 orci ( 5 < 6 ∨ 5 = 6 )
82 2 77 78 9 29 79 81 bpos1lem ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
83 3prm 3 ∈ ℙ
84 2lt3 2 < 3
85 68 orci ( 3 < 4 ∨ 3 = 4 )
86 2 82 83 26 42 84 85 bpos1lem ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
87 2prm 2 ∈ ℙ
88 eqid 2 = 2
89 88 olci ( 2 < 2 ∨ 2 = 2 )
90 2 86 87 50 54 56 89 bpos1lem ( 𝑁 ∈ ( ℤ ‘ 1 ) → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
91 1 90 sylbi ( 𝑁 ∈ ℕ → ( 𝑁 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) ) )
92 91 imp ( ( 𝑁 ∈ ℕ ∧ 𝑁 6 4 ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) )