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 mullidi ⊢ ( 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 · 𝑁 ) ) )