Proof of Theorem 257prm
| Step | Hyp | Ref
| Expression |
| 1 | | 2nn0 12543 |
. . . 4
⊢ 2 ∈
ℕ0 |
| 2 | | 5nn0 12546 |
. . . 4
⊢ 5 ∈
ℕ0 |
| 3 | 1, 2 | deccl 12748 |
. . 3
⊢ ;25 ∈
ℕ0 |
| 4 | | 7nn 12358 |
. . 3
⊢ 7 ∈
ℕ |
| 5 | 3, 4 | decnncl 12753 |
. 2
⊢ ;;257 ∈ ℕ |
| 6 | | 8nn0 12549 |
. . 3
⊢ 8 ∈
ℕ0 |
| 7 | | 4nn0 12545 |
. . 3
⊢ 4 ∈
ℕ0 |
| 8 | | 7nn0 12548 |
. . 3
⊢ 7 ∈
ℕ0 |
| 9 | | 1nn0 12542 |
. . 3
⊢ 1 ∈
ℕ0 |
| 10 | | 2lt8 12463 |
. . 3
⊢ 2 <
8 |
| 11 | | 5lt10 12868 |
. . 3
⊢ 5 <
;10 |
| 12 | | 7lt10 12866 |
. . 3
⊢ 7 <
;10 |
| 13 | 1, 6, 2, 7, 8, 9, 10, 11, 12 | 3decltc 12766 |
. 2
⊢ ;;257 < ;;841 |
| 14 | | 5nn 12352 |
. . . 4
⊢ 5 ∈
ℕ |
| 15 | 1, 14 | decnncl 12753 |
. . 3
⊢ ;25 ∈ ℕ |
| 16 | | 1lt10 12872 |
. . 3
⊢ 1 <
;10 |
| 17 | 15, 8, 9, 16 | declti 12771 |
. 2
⊢ 1 <
;;257 |
| 18 | | 3nn0 12544 |
. . 3
⊢ 3 ∈
ℕ0 |
| 19 | | 3t2e6 12432 |
. . 3
⊢ (3
· 2) = 6 |
| 20 | | df-7 12334 |
. . 3
⊢ 7 = (6 +
1) |
| 21 | 3, 18, 19, 20 | dec2dvds 17101 |
. 2
⊢ ¬ 2
∥ ;;257 |
| 22 | | 3nn 12345 |
. . . 4
⊢ 3 ∈
ℕ |
| 23 | | 2nn 12339 |
. . . 4
⊢ 2 ∈
ℕ |
| 24 | | 3cn 12347 |
. . . . . . 7
⊢ 3 ∈
ℂ |
| 25 | 24 | mulridi 11265 |
. . . . . 6
⊢ (3
· 1) = 3 |
| 26 | 25 | oveq1i 7441 |
. . . . 5
⊢ ((3
· 1) + 2) = (3 + 2) |
| 27 | | 3p2e5 12417 |
. . . . 5
⊢ (3 + 2) =
5 |
| 28 | 26, 27 | eqtri 2765 |
. . . 4
⊢ ((3
· 1) + 2) = 5 |
| 29 | | 2lt3 12438 |
. . . 4
⊢ 2 <
3 |
| 30 | 22, 9, 23, 28, 29 | ndvdsi 16449 |
. . 3
⊢ ¬ 3
∥ 5 |
| 31 | 1, 2, 8 | 3dvds2dec 16370 |
. . . 4
⊢ (3
∥ ;;257 ↔ 3 ∥ ((2 + 5) + 7)) |
| 32 | | 5cn 12354 |
. . . . . . . 8
⊢ 5 ∈
ℂ |
| 33 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 34 | | 5p2e7 12422 |
. . . . . . . 8
⊢ (5 + 2) =
7 |
| 35 | 32, 33, 34 | addcomli 11453 |
. . . . . . 7
⊢ (2 + 5) =
7 |
| 36 | 35 | oveq1i 7441 |
. . . . . 6
⊢ ((2 + 5)
+ 7) = (7 + 7) |
| 37 | | 7p7e14 12812 |
. . . . . 6
⊢ (7 + 7) =
;14 |
| 38 | 36, 37 | eqtri 2765 |
. . . . 5
⊢ ((2 + 5)
+ 7) = ;14 |
| 39 | 38 | breq2i 5151 |
. . . 4
⊢ (3
∥ ((2 + 5) + 7) ↔ 3 ∥ ;14) |
| 40 | 9, 7 | 3dvdsdec 16369 |
. . . . 5
⊢ (3
∥ ;14 ↔ 3 ∥ (1 +
4)) |
| 41 | | 4cn 12351 |
. . . . . . 7
⊢ 4 ∈
ℂ |
| 42 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 43 | | 4p1e5 12412 |
. . . . . . 7
⊢ (4 + 1) =
5 |
| 44 | 41, 42, 43 | addcomli 11453 |
. . . . . 6
⊢ (1 + 4) =
5 |
| 45 | 44 | breq2i 5151 |
. . . . 5
⊢ (3
∥ (1 + 4) ↔ 3 ∥ 5) |
| 46 | 40, 45 | bitri 275 |
. . . 4
⊢ (3
∥ ;14 ↔ 3 ∥
5) |
| 47 | 31, 39, 46 | 3bitri 297 |
. . 3
⊢ (3
∥ ;;257 ↔ 3 ∥ 5) |
| 48 | 30, 47 | mtbir 323 |
. 2
⊢ ¬ 3
∥ ;;257 |
| 49 | | 2lt5 12445 |
. . 3
⊢ 2 <
5 |
| 50 | 3, 23, 49, 34 | dec5dvds2 17103 |
. 2
⊢ ¬ 5
∥ ;;257 |
| 51 | | 6nn0 12547 |
. . . 4
⊢ 6 ∈
ℕ0 |
| 52 | 18, 51 | deccl 12748 |
. . 3
⊢ ;36 ∈
ℕ0 |
| 53 | | eqid 2737 |
. . . . 5
⊢ ;36 = ;36 |
| 54 | | 7t3e21 12843 |
. . . . . 6
⊢ (7
· 3) = ;21 |
| 55 | 1, 9, 7, 54, 44 | decaddi 12793 |
. . . . 5
⊢ ((7
· 3) + 4) = ;25 |
| 56 | | 7t6e42 12846 |
. . . . 5
⊢ (7
· 6) = ;42 |
| 57 | 8, 18, 51, 53, 1, 7, 55, 56 | decmul2c 12799 |
. . . 4
⊢ (7
· ;36) = ;;252 |
| 58 | 3, 1, 2, 57, 35 | decaddi 12793 |
. . 3
⊢ ((7
· ;36) + 5) = ;;257 |
| 59 | | 5lt7 12453 |
. . 3
⊢ 5 <
7 |
| 60 | 4, 52, 14, 58, 59 | ndvdsi 16449 |
. 2
⊢ ¬ 7
∥ ;;257 |
| 61 | | 1nn 12277 |
. . . 4
⊢ 1 ∈
ℕ |
| 62 | 9, 61 | decnncl 12753 |
. . 3
⊢ ;11 ∈ ℕ |
| 63 | 1, 18 | deccl 12748 |
. . 3
⊢ ;23 ∈
ℕ0 |
| 64 | | 4nn 12349 |
. . 3
⊢ 4 ∈
ℕ |
| 65 | 9, 9 | deccl 12748 |
. . . . 5
⊢ ;11 ∈
ℕ0 |
| 66 | | eqid 2737 |
. . . . 5
⊢ ;23 = ;23 |
| 67 | 65 | nn0cni 12538 |
. . . . . . . 8
⊢ ;11 ∈ ℂ |
| 68 | 67, 33 | mulcomi 11269 |
. . . . . . 7
⊢ (;11 · 2) = (2 · ;11) |
| 69 | 68 | oveq1i 7441 |
. . . . . 6
⊢ ((;11 · 2) + 3) = ((2 ·
;11) + 3) |
| 70 | 1 | 11multnc 12801 |
. . . . . . 7
⊢ (2
· ;11) = ;22 |
| 71 | 24, 33, 27 | addcomli 11453 |
. . . . . . 7
⊢ (2 + 3) =
5 |
| 72 | 1, 1, 18, 70, 71 | decaddi 12793 |
. . . . . 6
⊢ ((2
· ;11) + 3) = ;25 |
| 73 | 69, 72 | eqtri 2765 |
. . . . 5
⊢ ((;11 · 2) + 3) = ;25 |
| 74 | 18 | 11multnc 12801 |
. . . . . 6
⊢ (3
· ;11) = ;33 |
| 75 | 24, 67, 74 | mulcomli 11270 |
. . . . 5
⊢ (;11 · 3) = ;33 |
| 76 | 65, 1, 18, 66, 18, 18, 73, 75 | decmul2c 12799 |
. . . 4
⊢ (;11 · ;23) = ;;253 |
| 77 | | 4p3e7 12420 |
. . . . 5
⊢ (4 + 3) =
7 |
| 78 | 41, 24, 77 | addcomli 11453 |
. . . 4
⊢ (3 + 4) =
7 |
| 79 | 3, 18, 7, 76, 78 | decaddi 12793 |
. . 3
⊢ ((;11 · ;23) + 4) = ;;257 |
| 80 | | 4lt10 12869 |
. . . 4
⊢ 4 <
;10 |
| 81 | 61, 9, 7, 80 | declti 12771 |
. . 3
⊢ 4 <
;11 |
| 82 | 62, 63, 64, 79, 81 | ndvdsi 16449 |
. 2
⊢ ¬
;11 ∥ ;;257 |
| 83 | 9, 22 | decnncl 12753 |
. . 3
⊢ ;13 ∈ ℕ |
| 84 | | 9nn0 12550 |
. . . 4
⊢ 9 ∈
ℕ0 |
| 85 | 9, 84 | deccl 12748 |
. . 3
⊢ ;19 ∈
ℕ0 |
| 86 | | 10nn 12749 |
. . 3
⊢ ;10 ∈ ℕ |
| 87 | 9, 18 | deccl 12748 |
. . . . . . 7
⊢ ;13 ∈
ℕ0 |
| 88 | 87 | nn0cni 12538 |
. . . . . 6
⊢ ;13 ∈ ℂ |
| 89 | 85 | nn0cni 12538 |
. . . . . 6
⊢ ;19 ∈ ℂ |
| 90 | 88, 89 | mulcomi 11269 |
. . . . 5
⊢ (;13 · ;19) = (;19 · ;13) |
| 91 | 90 | oveq1i 7441 |
. . . 4
⊢ ((;13 · ;19) + ;10) = ((;19 · ;13) + ;10) |
| 92 | | 0nn0 12541 |
. . . . 5
⊢ 0 ∈
ℕ0 |
| 93 | | eqid 2737 |
. . . . 5
⊢ ;19 = ;19 |
| 94 | | eqid 2737 |
. . . . 5
⊢ ;10 = ;10 |
| 95 | 88 | mullidi 11266 |
. . . . . 6
⊢ (1
· ;13) = ;13 |
| 96 | | 1p1e2 12391 |
. . . . . . . 8
⊢ (1 + 1) =
2 |
| 97 | | eqid 2737 |
. . . . . . . 8
⊢ ;11 = ;11 |
| 98 | 9, 9, 96, 97 | decsuc 12764 |
. . . . . . 7
⊢ (;11 + 1) = ;12 |
| 99 | 67, 42, 98 | addcomli 11453 |
. . . . . 6
⊢ (1 +
;11) = ;12 |
| 100 | 9, 18, 9, 1, 95, 99, 96, 27 | decadd 12787 |
. . . . 5
⊢ ((1
· ;13) + (1 + ;11)) = ;25 |
| 101 | | eqid 2737 |
. . . . . . . 8
⊢ ;13 = ;13 |
| 102 | | 9cn 12366 |
. . . . . . . . . . 11
⊢ 9 ∈
ℂ |
| 103 | 102 | mulridi 11265 |
. . . . . . . . . 10
⊢ (9
· 1) = 9 |
| 104 | 103 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((9
· 1) + 2) = (9 + 2) |
| 105 | | 9p2e11 12820 |
. . . . . . . . 9
⊢ (9 + 2) =
;11 |
| 106 | 104, 105 | eqtri 2765 |
. . . . . . . 8
⊢ ((9
· 1) + 2) = ;11 |
| 107 | | 9t3e27 12856 |
. . . . . . . 8
⊢ (9
· 3) = ;27 |
| 108 | 84, 9, 18, 101, 8, 1, 106, 107 | decmul2c 12799 |
. . . . . . 7
⊢ (9
· ;13) = ;;117 |
| 109 | 108 | oveq1i 7441 |
. . . . . 6
⊢ ((9
· ;13) + 0) = (;;117 + 0) |
| 110 | 65, 8 | deccl 12748 |
. . . . . . . 8
⊢ ;;117 ∈ ℕ0 |
| 111 | 110 | nn0cni 12538 |
. . . . . . 7
⊢ ;;117 ∈ ℂ |
| 112 | 111 | addridi 11448 |
. . . . . 6
⊢ (;;117 + 0) = ;;117 |
| 113 | 109, 112 | eqtri 2765 |
. . . . 5
⊢ ((9
· ;13) + 0) = ;;117 |
| 114 | 9, 84, 9, 92, 93, 94, 87, 8, 65, 100, 113 | decmac 12785 |
. . . 4
⊢ ((;19 · ;13) + ;10) = ;;257 |
| 115 | 91, 114 | eqtri 2765 |
. . 3
⊢ ((;13 · ;19) + ;10) = ;;257 |
| 116 | | 3pos 12371 |
. . . 4
⊢ 0 <
3 |
| 117 | 9, 92, 22, 116 | declt 12761 |
. . 3
⊢ ;10 < ;13 |
| 118 | 83, 85, 86, 115, 117 | ndvdsi 16449 |
. 2
⊢ ¬
;13 ∥ ;;257 |
| 119 | 9, 4 | decnncl 12753 |
. . 3
⊢ ;17 ∈ ℕ |
| 120 | 9, 2 | deccl 12748 |
. . 3
⊢ ;15 ∈
ℕ0 |
| 121 | 9, 8 | deccl 12748 |
. . . . 5
⊢ ;17 ∈
ℕ0 |
| 122 | | eqid 2737 |
. . . . 5
⊢ ;15 = ;15 |
| 123 | 121 | nn0cni 12538 |
. . . . . . 7
⊢ ;17 ∈ ℂ |
| 124 | 123 | mulridi 11265 |
. . . . . 6
⊢ (;17 · 1) = ;17 |
| 125 | | 8cn 12363 |
. . . . . . 7
⊢ 8 ∈
ℂ |
| 126 | | 7cn 12360 |
. . . . . . 7
⊢ 7 ∈
ℂ |
| 127 | | 8p7e15 12818 |
. . . . . . 7
⊢ (8 + 7) =
;15 |
| 128 | 125, 126,
127 | addcomli 11453 |
. . . . . 6
⊢ (7 + 8) =
;15 |
| 129 | 9, 8, 6, 124, 96, 2, 128 | decaddci 12794 |
. . . . 5
⊢ ((;17 · 1) + 8) = ;25 |
| 130 | | eqid 2737 |
. . . . . 6
⊢ ;17 = ;17 |
| 131 | 32 | mullidi 11266 |
. . . . . . . 8
⊢ (1
· 5) = 5 |
| 132 | 131 | oveq1i 7441 |
. . . . . . 7
⊢ ((1
· 5) + 3) = (5 + 3) |
| 133 | | 5p3e8 12423 |
. . . . . . 7
⊢ (5 + 3) =
8 |
| 134 | 132, 133 | eqtri 2765 |
. . . . . 6
⊢ ((1
· 5) + 3) = 8 |
| 135 | | 7t5e35 12845 |
. . . . . 6
⊢ (7
· 5) = ;35 |
| 136 | 2, 9, 8, 130, 2, 18, 134, 135 | decmul1c 12798 |
. . . . 5
⊢ (;17 · 5) = ;85 |
| 137 | 121, 9, 2, 122, 2, 6, 129, 136 | decmul2c 12799 |
. . . 4
⊢ (;17 · ;15) = ;;255 |
| 138 | 3, 2, 1, 137, 34 | decaddi 12793 |
. . 3
⊢ ((;17 · ;15) + 2) = ;;257 |
| 139 | | 2lt10 12871 |
. . . 4
⊢ 2 <
;10 |
| 140 | 61, 8, 1, 139 | declti 12771 |
. . 3
⊢ 2 <
;17 |
| 141 | 119, 120,
23, 138, 140 | ndvdsi 16449 |
. 2
⊢ ¬
;17 ∥ ;;257 |
| 142 | | 9nn 12364 |
. . . 4
⊢ 9 ∈
ℕ |
| 143 | 9, 142 | decnncl 12753 |
. . 3
⊢ ;19 ∈ ℕ |
| 144 | | 9pos 12379 |
. . . 4
⊢ 0 <
9 |
| 145 | 9, 92, 142, 144 | declt 12761 |
. . 3
⊢ ;10 < ;19 |
| 146 | 143, 87, 86, 114, 145 | ndvdsi 16449 |
. 2
⊢ ¬
;19 ∥ ;;257 |
| 147 | 1, 22 | decnncl 12753 |
. . 3
⊢ ;23 ∈ ℕ |
| 148 | 65, 1, 18, 66, 18, 18, 72, 74 | decmul1c 12798 |
. . . 4
⊢ (;23 · ;11) = ;;253 |
| 149 | 3, 18, 7, 148, 78 | decaddi 12793 |
. . 3
⊢ ((;23 · ;11) + 4) = ;;257 |
| 150 | 23, 18, 7, 80 | declti 12771 |
. . 3
⊢ 4 <
;23 |
| 151 | 147, 65, 64, 149, 150 | ndvdsi 16449 |
. 2
⊢ ¬
;23 ∥ ;;257 |
| 152 | 5, 13, 17, 21, 48, 50, 60, 82, 118, 141, 146, 151 | prmlem2 17157 |
1
⊢ ;;257 ∈ ℙ |