Proof of Theorem bpos1
| Step | Hyp | Ref
| Expression |
| 1 | | elnnuz 12922 |
. . 3
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
| 2 | | ax-1 6 |
. . . 4
⊢
(∃𝑝 ∈
ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 3 | | 6nn0 12547 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℕ0 |
| 4 | | 4nn0 12545 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℕ0 |
| 5 | 3, 4 | deccl 12748 |
. . . . . . . . . . . . . . . 16
⊢ ;64 ∈
ℕ0 |
| 6 | 5 | nn0rei 12537 |
. . . . . . . . . . . . . . 15
⊢ ;64 ∈ ℝ |
| 7 | 6 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ ;64 ∈
ℝ) |
| 8 | | 8nn0 12549 |
. . . . . . . . . . . . . . . . 17
⊢ 8 ∈
ℕ0 |
| 9 | | 3nn0 12544 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℕ0 |
| 10 | 8, 9 | deccl 12748 |
. . . . . . . . . . . . . . . 16
⊢ ;83 ∈
ℕ0 |
| 11 | 10 | nn0rei 12537 |
. . . . . . . . . . . . . . 15
⊢ ;83 ∈ ℝ |
| 12 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ ;83 ∈
ℝ) |
| 13 | | eluzelre 12889 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ 𝑁 ∈
ℝ) |
| 14 | | 4lt10 12869 |
. . . . . . . . . . . . . . . 16
⊢ 4 <
;10 |
| 15 | | 6lt8 12459 |
. . . . . . . . . . . . . . . 16
⊢ 6 <
8 |
| 16 | 3, 8, 4, 9, 14, 15 | decltc 12762 |
. . . . . . . . . . . . . . 15
⊢ ;64 < ;83 |
| 17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ ;64 < ;83) |
| 18 | | eluzle 12891 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ ;83 ≤ 𝑁) |
| 19 | 7, 12, 13, 17, 18 | ltletrd 11421 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ ;64 < 𝑁) |
| 20 | | ltnle 11340 |
. . . . . . . . . . . . . 14
⊢ ((;64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (;64 < 𝑁 ↔ ¬ 𝑁 ≤ ;64)) |
| 21 | 6, 13, 20 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ (;64 < 𝑁 ↔ ¬ 𝑁 ≤ ;64)) |
| 22 | 19, 21 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ ¬ 𝑁 ≤ ;64) |
| 23 | 22 | pm2.21d 121 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘;83)
→ (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 24 | | 83prm 17160 |
. . . . . . . . . . 11
⊢ ;83 ∈ ℙ |
| 25 | 4, 9 | deccl 12748 |
. . . . . . . . . . 11
⊢ ;43 ∈
ℕ0 |
| 26 | | 2nn0 12543 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
| 27 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ;43 = ;43 |
| 28 | | 4t2e8 12434 |
. . . . . . . . . . . 12
⊢ (4
· 2) = 8 |
| 29 | | 3t2e6 12432 |
. . . . . . . . . . . 12
⊢ (3
· 2) = 6 |
| 30 | 26, 4, 9, 27, 28, 29 | decmul1 12797 |
. . . . . . . . . . 11
⊢ (;43 · 2) = ;86 |
| 31 | | 3lt10 12870 |
. . . . . . . . . . . 12
⊢ 3 <
;10 |
| 32 | | 4lt8 12461 |
. . . . . . . . . . . 12
⊢ 4 <
8 |
| 33 | 4, 8, 9, 9, 31, 32 | decltc 12762 |
. . . . . . . . . . 11
⊢ ;43 < ;83 |
| 34 | | 6nn 12355 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℕ |
| 35 | | 3lt6 12449 |
. . . . . . . . . . . . 13
⊢ 3 <
6 |
| 36 | 8, 9, 34, 35 | declt 12761 |
. . . . . . . . . . . 12
⊢ ;83 < ;86 |
| 37 | 36 | orci 866 |
. . . . . . . . . . 11
⊢ (;83 < ;86 ∨ ;83 = ;86) |
| 38 | 2, 23, 24, 25, 30, 33, 37 | bpos1lem 27326 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘;43)
→ (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 39 | | 43prm 17159 |
. . . . . . . . . 10
⊢ ;43 ∈ ℙ |
| 40 | 26, 9 | deccl 12748 |
. . . . . . . . . 10
⊢ ;23 ∈
ℕ0 |
| 41 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ;23 = ;23 |
| 42 | | 2t2e4 12430 |
. . . . . . . . . . 11
⊢ (2
· 2) = 4 |
| 43 | 26, 26, 9, 41, 42, 29 | decmul1 12797 |
. . . . . . . . . 10
⊢ (;23 · 2) = ;46 |
| 44 | | 2lt4 12441 |
. . . . . . . . . . 11
⊢ 2 <
4 |
| 45 | 26, 4, 9, 9, 31, 44 | decltc 12762 |
. . . . . . . . . 10
⊢ ;23 < ;43 |
| 46 | 4, 9, 34, 35 | declt 12761 |
. . . . . . . . . . 11
⊢ ;43 < ;46 |
| 47 | 46 | orci 866 |
. . . . . . . . . 10
⊢ (;43 < ;46 ∨ ;43 = ;46) |
| 48 | 2, 38, 39, 40, 43, 45, 47 | bpos1lem 27326 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘;23)
→ (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 49 | | 23prm 17156 |
. . . . . . . . 9
⊢ ;23 ∈ ℙ |
| 50 | | 1nn0 12542 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
| 51 | 50, 9 | deccl 12748 |
. . . . . . . . 9
⊢ ;13 ∈
ℕ0 |
| 52 | | eqid 2737 |
. . . . . . . . . 10
⊢ ;13 = ;13 |
| 53 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 54 | 53 | mullidi 11266 |
. . . . . . . . . 10
⊢ (1
· 2) = 2 |
| 55 | 26, 50, 9, 52, 54, 29 | decmul1 12797 |
. . . . . . . . 9
⊢ (;13 · 2) = ;26 |
| 56 | | 1lt2 12437 |
. . . . . . . . . 10
⊢ 1 <
2 |
| 57 | 50, 26, 9, 9, 31, 56 | decltc 12762 |
. . . . . . . . 9
⊢ ;13 < ;23 |
| 58 | 26, 9, 34, 35 | declt 12761 |
. . . . . . . . . 10
⊢ ;23 < ;26 |
| 59 | 58 | orci 866 |
. . . . . . . . 9
⊢ (;23 < ;26 ∨ ;23 = ;26) |
| 60 | 2, 48, 49, 51, 55, 57, 59 | bpos1lem 27326 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘;13)
→ (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 61 | | 13prm 17153 |
. . . . . . . 8
⊢ ;13 ∈ ℙ |
| 62 | | 7nn0 12548 |
. . . . . . . 8
⊢ 7 ∈
ℕ0 |
| 63 | | 7t2e14 12842 |
. . . . . . . 8
⊢ (7
· 2) = ;14 |
| 64 | | 1nn 12277 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
| 65 | | 7lt10 12866 |
. . . . . . . . 9
⊢ 7 <
;10 |
| 66 | 64, 9, 62, 65 | declti 12771 |
. . . . . . . 8
⊢ 7 <
;13 |
| 67 | | 4nn 12349 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ |
| 68 | | 3lt4 12440 |
. . . . . . . . . 10
⊢ 3 <
4 |
| 69 | 50, 9, 67, 68 | declt 12761 |
. . . . . . . . 9
⊢ ;13 < ;14 |
| 70 | 69 | orci 866 |
. . . . . . . 8
⊢ (;13 < ;14 ∨ ;13 = ;14) |
| 71 | 2, 60, 61, 62, 63, 66, 70 | bpos1lem 27326 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘7) → (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 72 | | 7prm 17148 |
. . . . . . 7
⊢ 7 ∈
ℙ |
| 73 | | 5nn0 12546 |
. . . . . . 7
⊢ 5 ∈
ℕ0 |
| 74 | | 5t2e10 12833 |
. . . . . . 7
⊢ (5
· 2) = ;10 |
| 75 | | 5lt7 12453 |
. . . . . . 7
⊢ 5 <
7 |
| 76 | 65 | orci 866 |
. . . . . . 7
⊢ (7 <
;10 ∨ 7 = ;10) |
| 77 | 2, 71, 72, 73, 74, 75, 76 | bpos1lem 27326 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘5) → (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 78 | | 5prm 17146 |
. . . . . 6
⊢ 5 ∈
ℙ |
| 79 | | 3lt5 12444 |
. . . . . 6
⊢ 3 <
5 |
| 80 | | 5lt6 12447 |
. . . . . . 7
⊢ 5 <
6 |
| 81 | 80 | orci 866 |
. . . . . 6
⊢ (5 < 6
∨ 5 = 6) |
| 82 | 2, 77, 78, 9, 29, 79, 81 | bpos1lem 27326 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 83 | | 3prm 16731 |
. . . . 5
⊢ 3 ∈
ℙ |
| 84 | | 2lt3 12438 |
. . . . 5
⊢ 2 <
3 |
| 85 | 68 | orci 866 |
. . . . 5
⊢ (3 < 4
∨ 3 = 4) |
| 86 | 2, 82, 83, 26, 42, 84, 85 | bpos1lem 27326 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 87 | | 2prm 16729 |
. . . 4
⊢ 2 ∈
ℙ |
| 88 | | eqid 2737 |
. . . . 5
⊢ 2 =
2 |
| 89 | 88 | olci 867 |
. . . 4
⊢ (2 < 2
∨ 2 = 2) |
| 90 | 2, 86, 87, 50, 54, 56, 89 | bpos1lem 27326 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 91 | 1, 90 | sylbi 217 |
. 2
⊢ (𝑁 ∈ ℕ → (𝑁 ≤ ;64 → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))) |
| 92 | 91 | imp 406 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≤ ;64) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) |