| Step | Hyp | Ref
| Expression |
| 1 | | prmlem2.n |
. 2
⊢ 𝑁 ∈ ℕ |
| 2 | | prmlem2.gt |
. 2
⊢ 1 <
𝑁 |
| 3 | | prmlem2.2 |
. 2
⊢ ¬ 2
∥ 𝑁 |
| 4 | | prmlem2.3 |
. 2
⊢ ¬ 3
∥ 𝑁 |
| 5 | | eluzelre 12889 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ 𝑥 ∈
ℝ) |
| 6 | 5 | resqcld 14165 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ (𝑥↑2) ∈
ℝ) |
| 7 | | eluzle 12891 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ ;29 ≤ 𝑥) |
| 8 | | 2nn0 12543 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℕ0 |
| 9 | | 9nn0 12550 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 9 ∈
ℕ0 |
| 10 | 8, 9 | deccl 12748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ;29 ∈
ℕ0 |
| 11 | 10 | nn0rei 12537 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ;29 ∈ ℝ |
| 12 | 10 | nn0ge0i 12553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ≤
;29 |
| 13 | | le2sq2 14175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((;29 ∈ ℝ ∧ 0 ≤ ;29) ∧ (𝑥 ∈ ℝ ∧ ;29 ≤ 𝑥)) → (;29↑2) ≤ (𝑥↑2)) |
| 14 | 11, 12, 13 | mpanl12 702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ ;29 ≤ 𝑥) → (;29↑2) ≤ (𝑥↑2)) |
| 15 | 5, 7, 14 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ (;29↑2) ≤ (𝑥↑2)) |
| 16 | 1 | nnrei 12275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑁 ∈ ℝ |
| 17 | 11 | resqcli 14225 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (;29↑2) ∈
ℝ |
| 18 | | prmlem2.lt |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑁 < ;;841 |
| 19 | 10 | nn0cni 12538 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ;29 ∈ ℂ |
| 20 | 19 | sqvali 14219 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (;29↑2) = (;29 · ;29) |
| 21 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ;29 = ;29 |
| 22 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℕ0 |
| 23 | | 6nn0 12547 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 6 ∈
ℕ0 |
| 24 | 8, 23 | deccl 12748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ;26 ∈
ℕ0 |
| 25 | | 5nn0 12546 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 5 ∈
ℕ0 |
| 26 | | 8nn0 12549 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 8 ∈
ℕ0 |
| 27 | 19 | 2timesi 12404 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (2
· ;29) = (;29 + ;29) |
| 28 | | 2p2e4 12401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (2 + 2) =
4 |
| 29 | 28 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((2 + 2)
+ 1) = (4 + 1) |
| 30 | | 4p1e5 12412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (4 + 1) =
5 |
| 31 | 29, 30 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((2 + 2)
+ 1) = 5 |
| 32 | | 9p9e18 12827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (9 + 9) =
;18 |
| 33 | 8, 9, 8, 9, 21, 21, 31, 26, 32 | decaddc 12788 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (;29 + ;29) = ;58 |
| 34 | 27, 33 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2
· ;29) = ;58 |
| 35 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ;26 = ;26 |
| 36 | | 5p2e7 12422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (5 + 2) =
7 |
| 37 | 36 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((5 + 2)
+ 1) = (7 + 1) |
| 38 | | 7p1e8 12415 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (7 + 1) =
8 |
| 39 | 37, 38 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((5 + 2)
+ 1) = 8 |
| 40 | | 4nn0 12545 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 4 ∈
ℕ0 |
| 41 | | 8p6e14 12817 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (8 + 6) =
;14 |
| 42 | 25, 26, 8, 23, 34, 35, 39, 40, 41 | decaddc 12788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
· ;29) + ;26) = ;84 |
| 43 | | 9t2e18 12855 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (9
· 2) = ;18 |
| 44 | | 1p1e2 12391 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 + 1) =
2 |
| 45 | | 8p8e16 12819 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (8 + 8) =
;16 |
| 46 | 22, 26, 26, 43, 44, 23, 45 | decaddci 12794 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((9
· 2) + 8) = ;26 |
| 47 | | 9t9e81 12862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (9
· 9) = ;81 |
| 48 | 9, 8, 9, 21, 22, 26, 46, 47 | decmul2c 12799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (9
· ;29) = ;;261 |
| 49 | 10, 8, 9, 21, 22, 24, 42, 48 | decmul1c 12798 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (;29 · ;29) = ;;841 |
| 50 | 20, 49 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (;29↑2) = ;;841 |
| 51 | 18, 50 | breqtrri 5170 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑁 < (;29↑2) |
| 52 | | ltletr 11353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℝ ∧ (;29↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) →
((𝑁 < (;29↑2) ∧ (;29↑2) ≤ (𝑥↑2)) → 𝑁 < (𝑥↑2))) |
| 53 | 51, 52 | mpani 696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℝ ∧ (;29↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) →
((;29↑2) ≤ (𝑥↑2) → 𝑁 < (𝑥↑2))) |
| 54 | 16, 17, 53 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥↑2) ∈ ℝ →
((;29↑2) ≤ (𝑥↑2) → 𝑁 < (𝑥↑2))) |
| 55 | 6, 15, 54 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ 𝑁 < (𝑥↑2)) |
| 56 | | ltnle 11340 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) →
(𝑁 < (𝑥↑2) ↔ ¬ (𝑥↑2) ≤ 𝑁)) |
| 57 | 16, 6, 56 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ (𝑁 < (𝑥↑2) ↔ ¬ (𝑥↑2) ≤ 𝑁)) |
| 58 | 55, 57 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ ¬ (𝑥↑2)
≤ 𝑁) |
| 59 | 58 | pm2.21d 121 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ ((𝑥↑2) ≤
𝑁 → ¬ 𝑥 ∥ 𝑁)) |
| 60 | 59 | adantld 490 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
(ℤ≥‘;29)
→ ((𝑥 ∈ (ℙ
∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 61 | 60 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((¬ 2
∥ ;29 ∧ 𝑥 ∈
(ℤ≥‘;29)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 62 | | 9nn 12364 |
. . . . . . . . . . . . . . . 16
⊢ 9 ∈
ℕ |
| 63 | | 3nn 12345 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℕ |
| 64 | | 1lt9 12472 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
9 |
| 65 | | 1lt3 12439 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
3 |
| 66 | | 9t3e27 12856 |
. . . . . . . . . . . . . . . 16
⊢ (9
· 3) = ;27 |
| 67 | 62, 63, 64, 65, 66 | nprmi 16726 |
. . . . . . . . . . . . . . 15
⊢ ¬
;27 ∈
ℙ |
| 68 | 67 | pm2.21i 119 |
. . . . . . . . . . . . . 14
⊢ (;27 ∈ ℙ → ¬ ;27 ∥ 𝑁) |
| 69 | | 7nn0 12548 |
. . . . . . . . . . . . . . 15
⊢ 7 ∈
ℕ0 |
| 70 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ ;27 = ;27 |
| 71 | | 7p2e9 12427 |
. . . . . . . . . . . . . . 15
⊢ (7 + 2) =
9 |
| 72 | 8, 69, 8, 70, 71 | decaddi 12793 |
. . . . . . . . . . . . . 14
⊢ (;27 + 2) = ;29 |
| 73 | 61, 68, 72 | prmlem0 17143 |
. . . . . . . . . . . . 13
⊢ ((¬ 2
∥ ;27 ∧ 𝑥 ∈
(ℤ≥‘;27)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 74 | | 5nn 12352 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℕ |
| 75 | | 1lt5 12446 |
. . . . . . . . . . . . . . 15
⊢ 1 <
5 |
| 76 | | 5t5e25 12836 |
. . . . . . . . . . . . . . 15
⊢ (5
· 5) = ;25 |
| 77 | 74, 74, 75, 75, 76 | nprmi 16726 |
. . . . . . . . . . . . . 14
⊢ ¬
;25 ∈
ℙ |
| 78 | 77 | pm2.21i 119 |
. . . . . . . . . . . . 13
⊢ (;25 ∈ ℙ → ¬ ;25 ∥ 𝑁) |
| 79 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ ;25 = ;25 |
| 80 | 8, 25, 8, 79, 36 | decaddi 12793 |
. . . . . . . . . . . . 13
⊢ (;25 + 2) = ;27 |
| 81 | 73, 78, 80 | prmlem0 17143 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ ;25 ∧ 𝑥 ∈
(ℤ≥‘;25)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 82 | | prmlem2.23 |
. . . . . . . . . . . . 13
⊢ ¬
;23 ∥ 𝑁 |
| 83 | 82 | a1i 11 |
. . . . . . . . . . . 12
⊢ (;23 ∈ ℙ → ¬ ;23 ∥ 𝑁) |
| 84 | | 3nn0 12544 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ0 |
| 85 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ;23 = ;23 |
| 86 | | 3p2e5 12417 |
. . . . . . . . . . . . 13
⊢ (3 + 2) =
5 |
| 87 | 8, 84, 8, 85, 86 | decaddi 12793 |
. . . . . . . . . . . 12
⊢ (;23 + 2) = ;25 |
| 88 | 81, 83, 87 | prmlem0 17143 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ ;23 ∧ 𝑥 ∈
(ℤ≥‘;23)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 89 | | 7nn 12358 |
. . . . . . . . . . . . 13
⊢ 7 ∈
ℕ |
| 90 | | 1lt7 12457 |
. . . . . . . . . . . . 13
⊢ 1 <
7 |
| 91 | | 7t3e21 12843 |
. . . . . . . . . . . . 13
⊢ (7
· 3) = ;21 |
| 92 | 89, 63, 90, 65, 91 | nprmi 16726 |
. . . . . . . . . . . 12
⊢ ¬
;21 ∈
ℙ |
| 93 | 92 | pm2.21i 119 |
. . . . . . . . . . 11
⊢ (;21 ∈ ℙ → ¬ ;21 ∥ 𝑁) |
| 94 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ;21 = ;21 |
| 95 | | 1p2e3 12409 |
. . . . . . . . . . . 12
⊢ (1 + 2) =
3 |
| 96 | 8, 22, 8, 94, 95 | decaddi 12793 |
. . . . . . . . . . 11
⊢ (;21 + 2) = ;23 |
| 97 | 88, 93, 96 | prmlem0 17143 |
. . . . . . . . . 10
⊢ ((¬ 2
∥ ;21 ∧ 𝑥 ∈
(ℤ≥‘;21)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 98 | | prmlem2.19 |
. . . . . . . . . . 11
⊢ ¬
;19 ∥ 𝑁 |
| 99 | 98 | a1i 11 |
. . . . . . . . . 10
⊢ (;19 ∈ ℙ → ¬ ;19 ∥ 𝑁) |
| 100 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ;19 = ;19 |
| 101 | | 9p2e11 12820 |
. . . . . . . . . . 11
⊢ (9 + 2) =
;11 |
| 102 | 22, 9, 8, 100, 44, 22, 101 | decaddci 12794 |
. . . . . . . . . 10
⊢ (;19 + 2) = ;21 |
| 103 | 97, 99, 102 | prmlem0 17143 |
. . . . . . . . 9
⊢ ((¬ 2
∥ ;19 ∧ 𝑥 ∈
(ℤ≥‘;19)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 104 | | prmlem2.17 |
. . . . . . . . . 10
⊢ ¬
;17 ∥ 𝑁 |
| 105 | 104 | a1i 11 |
. . . . . . . . 9
⊢ (;17 ∈ ℙ → ¬ ;17 ∥ 𝑁) |
| 106 | | eqid 2737 |
. . . . . . . . . 10
⊢ ;17 = ;17 |
| 107 | 22, 69, 8, 106, 71 | decaddi 12793 |
. . . . . . . . 9
⊢ (;17 + 2) = ;19 |
| 108 | 103, 105,
107 | prmlem0 17143 |
. . . . . . . 8
⊢ ((¬ 2
∥ ;17 ∧ 𝑥 ∈
(ℤ≥‘;17)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 109 | | 5t3e15 12834 |
. . . . . . . . . 10
⊢ (5
· 3) = ;15 |
| 110 | 74, 63, 75, 65, 109 | nprmi 16726 |
. . . . . . . . 9
⊢ ¬
;15 ∈
ℙ |
| 111 | 110 | pm2.21i 119 |
. . . . . . . 8
⊢ (;15 ∈ ℙ → ¬ ;15 ∥ 𝑁) |
| 112 | | eqid 2737 |
. . . . . . . . 9
⊢ ;15 = ;15 |
| 113 | 22, 25, 8, 112, 36 | decaddi 12793 |
. . . . . . . 8
⊢ (;15 + 2) = ;17 |
| 114 | 108, 111,
113 | prmlem0 17143 |
. . . . . . 7
⊢ ((¬ 2
∥ ;15 ∧ 𝑥 ∈
(ℤ≥‘;15)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 115 | | prmlem2.13 |
. . . . . . . 8
⊢ ¬
;13 ∥ 𝑁 |
| 116 | 115 | a1i 11 |
. . . . . . 7
⊢ (;13 ∈ ℙ → ¬ ;13 ∥ 𝑁) |
| 117 | | eqid 2737 |
. . . . . . . 8
⊢ ;13 = ;13 |
| 118 | 22, 84, 8, 117, 86 | decaddi 12793 |
. . . . . . 7
⊢ (;13 + 2) = ;15 |
| 119 | 114, 116,
118 | prmlem0 17143 |
. . . . . 6
⊢ ((¬ 2
∥ ;13 ∧ 𝑥 ∈
(ℤ≥‘;13)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 120 | | prmlem2.11 |
. . . . . . 7
⊢ ¬
;11 ∥ 𝑁 |
| 121 | 120 | a1i 11 |
. . . . . 6
⊢ (;11 ∈ ℙ → ¬ ;11 ∥ 𝑁) |
| 122 | | eqid 2737 |
. . . . . . 7
⊢ ;11 = ;11 |
| 123 | 22, 22, 8, 122, 95 | decaddi 12793 |
. . . . . 6
⊢ (;11 + 2) = ;13 |
| 124 | 119, 121,
123 | prmlem0 17143 |
. . . . 5
⊢ ((¬ 2
∥ ;11 ∧ 𝑥 ∈
(ℤ≥‘;11)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 125 | | 9nprm 17150 |
. . . . . 6
⊢ ¬ 9
∈ ℙ |
| 126 | 125 | pm2.21i 119 |
. . . . 5
⊢ (9 ∈
ℙ → ¬ 9 ∥ 𝑁) |
| 127 | 124, 126,
101 | prmlem0 17143 |
. . . 4
⊢ ((¬ 2
∥ 9 ∧ 𝑥 ∈
(ℤ≥‘9)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 128 | | prmlem2.7 |
. . . . 5
⊢ ¬ 7
∥ 𝑁 |
| 129 | 128 | a1i 11 |
. . . 4
⊢ (7 ∈
ℙ → ¬ 7 ∥ 𝑁) |
| 130 | 127, 129,
71 | prmlem0 17143 |
. . 3
⊢ ((¬ 2
∥ 7 ∧ 𝑥 ∈
(ℤ≥‘7)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 131 | | prmlem2.5 |
. . . 4
⊢ ¬ 5
∥ 𝑁 |
| 132 | 131 | a1i 11 |
. . 3
⊢ (5 ∈
ℙ → ¬ 5 ∥ 𝑁) |
| 133 | 130, 132,
36 | prmlem0 17143 |
. 2
⊢ ((¬ 2
∥ 5 ∧ 𝑥 ∈
(ℤ≥‘5)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
| 134 | 1, 2, 3, 4, 133 | prmlem1a 17144 |
1
⊢ 𝑁 ∈ ℙ |