Proof of Theorem 317prm
| Step | Hyp | Ref
| Expression |
| 1 | | 3nn0 12544 |
. . . 4
⊢ 3 ∈
ℕ0 |
| 2 | | 1nn0 12542 |
. . . 4
⊢ 1 ∈
ℕ0 |
| 3 | 1, 2 | deccl 12748 |
. . 3
⊢ ;31 ∈
ℕ0 |
| 4 | | 7nn 12358 |
. . 3
⊢ 7 ∈
ℕ |
| 5 | 3, 4 | decnncl 12753 |
. 2
⊢ ;;317 ∈ ℕ |
| 6 | | 8nn0 12549 |
. . 3
⊢ 8 ∈
ℕ0 |
| 7 | | 4nn0 12545 |
. . 3
⊢ 4 ∈
ℕ0 |
| 8 | | 7nn0 12548 |
. . 3
⊢ 7 ∈
ℕ0 |
| 9 | | 3lt8 12462 |
. . 3
⊢ 3 <
8 |
| 10 | | 1lt10 12872 |
. . 3
⊢ 1 <
;10 |
| 11 | | 7lt10 12866 |
. . 3
⊢ 7 <
;10 |
| 12 | 1, 6, 2, 7, 8, 2, 9, 10, 11 | 3decltc 12766 |
. 2
⊢ ;;317 < ;;841 |
| 13 | | 1nn 12277 |
. . . 4
⊢ 1 ∈
ℕ |
| 14 | 1, 13 | decnncl 12753 |
. . 3
⊢ ;31 ∈ ℕ |
| 15 | 14, 8, 2, 10 | declti 12771 |
. 2
⊢ 1 <
;;317 |
| 16 | | 3t2e6 12432 |
. . 3
⊢ (3
· 2) = 6 |
| 17 | | df-7 12334 |
. . 3
⊢ 7 = (6 +
1) |
| 18 | 3, 1, 16, 17 | dec2dvds 17101 |
. 2
⊢ ¬ 2
∥ ;;317 |
| 19 | | 3nn 12345 |
. . 3
⊢ 3 ∈
ℕ |
| 20 | | 10nn0 12751 |
. . . 4
⊢ ;10 ∈
ℕ0 |
| 21 | | 5nn0 12546 |
. . . 4
⊢ 5 ∈
ℕ0 |
| 22 | 20, 21 | deccl 12748 |
. . 3
⊢ ;;105 ∈ ℕ0 |
| 23 | | 2nn 12339 |
. . 3
⊢ 2 ∈
ℕ |
| 24 | | 0nn0 12541 |
. . . 4
⊢ 0 ∈
ℕ0 |
| 25 | | 2nn0 12543 |
. . . 4
⊢ 2 ∈
ℕ0 |
| 26 | | eqid 2737 |
. . . 4
⊢ ;;105 = ;;105 |
| 27 | 25 | dec0h 12755 |
. . . 4
⊢ 2 = ;02 |
| 28 | | eqid 2737 |
. . . . 5
⊢ ;10 = ;10 |
| 29 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 30 | 29 | addlidi 11449 |
. . . . . 6
⊢ (0 + 1) =
1 |
| 31 | 2 | dec0h 12755 |
. . . . . 6
⊢ 1 = ;01 |
| 32 | 30, 31 | eqtri 2765 |
. . . . 5
⊢ (0 + 1) =
;01 |
| 33 | | 3cn 12347 |
. . . . . . . 8
⊢ 3 ∈
ℂ |
| 34 | 33 | mulridi 11265 |
. . . . . . 7
⊢ (3
· 1) = 3 |
| 35 | | 00id 11436 |
. . . . . . 7
⊢ (0 + 0) =
0 |
| 36 | 34, 35 | oveq12i 7443 |
. . . . . 6
⊢ ((3
· 1) + (0 + 0)) = (3 + 0) |
| 37 | 33 | addridi 11448 |
. . . . . 6
⊢ (3 + 0) =
3 |
| 38 | 36, 37 | eqtri 2765 |
. . . . 5
⊢ ((3
· 1) + (0 + 0)) = 3 |
| 39 | 33 | mul01i 11451 |
. . . . . . . 8
⊢ (3
· 0) = 0 |
| 40 | 39 | oveq1i 7441 |
. . . . . . 7
⊢ ((3
· 0) + 1) = (0 + 1) |
| 41 | 40, 30 | eqtri 2765 |
. . . . . 6
⊢ ((3
· 0) + 1) = 1 |
| 42 | 41, 31 | eqtri 2765 |
. . . . 5
⊢ ((3
· 0) + 1) = ;01 |
| 43 | 2, 24, 24, 2, 28, 32, 1, 2, 24, 38, 42 | decma2c 12786 |
. . . 4
⊢ ((3
· ;10) + (0 + 1)) = ;31 |
| 44 | | 5cn 12354 |
. . . . . 6
⊢ 5 ∈
ℂ |
| 45 | | 5t3e15 12834 |
. . . . . 6
⊢ (5
· 3) = ;15 |
| 46 | 44, 33, 45 | mulcomli 11270 |
. . . . 5
⊢ (3
· 5) = ;15 |
| 47 | | 5p2e7 12422 |
. . . . 5
⊢ (5 + 2) =
7 |
| 48 | 2, 21, 25, 46, 47 | decaddi 12793 |
. . . 4
⊢ ((3
· 5) + 2) = ;17 |
| 49 | 20, 21, 24, 25, 26, 27, 1, 8, 2,
43, 48 | decma2c 12786 |
. . 3
⊢ ((3
· ;;105) + 2) = ;;317 |
| 50 | | 2lt3 12438 |
. . 3
⊢ 2 <
3 |
| 51 | 19, 22, 23, 49, 50 | ndvdsi 16449 |
. 2
⊢ ¬ 3
∥ ;;317 |
| 52 | | 2lt5 12445 |
. . 3
⊢ 2 <
5 |
| 53 | 3, 23, 52, 47 | dec5dvds2 17103 |
. 2
⊢ ¬ 5
∥ ;;317 |
| 54 | 7, 21 | deccl 12748 |
. . 3
⊢ ;45 ∈
ℕ0 |
| 55 | | eqid 2737 |
. . . 4
⊢ ;45 = ;45 |
| 56 | 33 | addlidi 11449 |
. . . . . 6
⊢ (0 + 3) =
3 |
| 57 | 56 | oveq2i 7442 |
. . . . 5
⊢ ((7
· 4) + (0 + 3)) = ((7 · 4) + 3) |
| 58 | | 7t4e28 12844 |
. . . . . 6
⊢ (7
· 4) = ;28 |
| 59 | | 2p1e3 12408 |
. . . . . 6
⊢ (2 + 1) =
3 |
| 60 | | 8p3e11 12814 |
. . . . . 6
⊢ (8 + 3) =
;11 |
| 61 | 25, 6, 1, 58, 59, 2, 60 | decaddci 12794 |
. . . . 5
⊢ ((7
· 4) + 3) = ;31 |
| 62 | 57, 61 | eqtri 2765 |
. . . 4
⊢ ((7
· 4) + (0 + 3)) = ;31 |
| 63 | | 7t5e35 12845 |
. . . . 5
⊢ (7
· 5) = ;35 |
| 64 | 1, 21, 25, 63, 47 | decaddi 12793 |
. . . 4
⊢ ((7
· 5) + 2) = ;37 |
| 65 | 7, 21, 24, 25, 55, 27, 8, 8, 1,
62, 64 | decma2c 12786 |
. . 3
⊢ ((7
· ;45) + 2) = ;;317 |
| 66 | | 2lt7 12456 |
. . 3
⊢ 2 <
7 |
| 67 | 4, 54, 23, 65, 66 | ndvdsi 16449 |
. 2
⊢ ¬ 7
∥ ;;317 |
| 68 | 2, 13 | decnncl 12753 |
. . 3
⊢ ;11 ∈ ℕ |
| 69 | 25, 6 | deccl 12748 |
. . 3
⊢ ;28 ∈
ℕ0 |
| 70 | | 9nn 12364 |
. . 3
⊢ 9 ∈
ℕ |
| 71 | | 9nn0 12550 |
. . . 4
⊢ 9 ∈
ℕ0 |
| 72 | | eqid 2737 |
. . . 4
⊢ ;28 = ;28 |
| 73 | 71 | dec0h 12755 |
. . . 4
⊢ 9 = ;09 |
| 74 | 2, 2 | deccl 12748 |
. . . 4
⊢ ;11 ∈
ℕ0 |
| 75 | | eqid 2737 |
. . . . 5
⊢ ;11 = ;11 |
| 76 | | 9cn 12366 |
. . . . . . 7
⊢ 9 ∈
ℂ |
| 77 | 76 | addlidi 11449 |
. . . . . 6
⊢ (0 + 9) =
9 |
| 78 | 77, 73 | eqtri 2765 |
. . . . 5
⊢ (0 + 9) =
;09 |
| 79 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 80 | 79 | mullidi 11266 |
. . . . . . 7
⊢ (1
· 2) = 2 |
| 81 | 80, 30 | oveq12i 7443 |
. . . . . 6
⊢ ((1
· 2) + (0 + 1)) = (2 + 1) |
| 82 | 81, 59 | eqtri 2765 |
. . . . 5
⊢ ((1
· 2) + (0 + 1)) = 3 |
| 83 | 80 | oveq1i 7441 |
. . . . . 6
⊢ ((1
· 2) + 9) = (2 + 9) |
| 84 | | 9p2e11 12820 |
. . . . . . 7
⊢ (9 + 2) =
;11 |
| 85 | 76, 79, 84 | addcomli 11453 |
. . . . . 6
⊢ (2 + 9) =
;11 |
| 86 | 83, 85 | eqtri 2765 |
. . . . 5
⊢ ((1
· 2) + 9) = ;11 |
| 87 | 2, 2, 24, 71, 75, 78, 25, 2, 2, 82, 86 | decmac 12785 |
. . . 4
⊢ ((;11 · 2) + (0 + 9)) = ;31 |
| 88 | | 8cn 12363 |
. . . . . . . 8
⊢ 8 ∈
ℂ |
| 89 | 88 | mullidi 11266 |
. . . . . . 7
⊢ (1
· 8) = 8 |
| 90 | 89, 30 | oveq12i 7443 |
. . . . . 6
⊢ ((1
· 8) + (0 + 1)) = (8 + 1) |
| 91 | | 8p1e9 12416 |
. . . . . 6
⊢ (8 + 1) =
9 |
| 92 | 90, 91 | eqtri 2765 |
. . . . 5
⊢ ((1
· 8) + (0 + 1)) = 9 |
| 93 | 89 | oveq1i 7441 |
. . . . . 6
⊢ ((1
· 8) + 9) = (8 + 9) |
| 94 | | 9p8e17 12826 |
. . . . . . 7
⊢ (9 + 8) =
;17 |
| 95 | 76, 88, 94 | addcomli 11453 |
. . . . . 6
⊢ (8 + 9) =
;17 |
| 96 | 93, 95 | eqtri 2765 |
. . . . 5
⊢ ((1
· 8) + 9) = ;17 |
| 97 | 2, 2, 24, 71, 75, 73, 6, 8, 2,
92, 96 | decmac 12785 |
. . . 4
⊢ ((;11 · 8) + 9) = ;97 |
| 98 | 25, 6, 24, 71, 72, 73, 74, 8, 71, 87, 97 | decma2c 12786 |
. . 3
⊢ ((;11 · ;28) + 9) = ;;317 |
| 99 | | 9lt10 12864 |
. . . 4
⊢ 9 <
;10 |
| 100 | 13, 2, 71, 99 | declti 12771 |
. . 3
⊢ 9 <
;11 |
| 101 | 68, 69, 70, 98, 100 | ndvdsi 16449 |
. 2
⊢ ¬
;11 ∥ ;;317 |
| 102 | 2, 19 | decnncl 12753 |
. . 3
⊢ ;13 ∈ ℕ |
| 103 | 25, 7 | deccl 12748 |
. . 3
⊢ ;24 ∈
ℕ0 |
| 104 | | 5nn 12352 |
. . 3
⊢ 5 ∈
ℕ |
| 105 | | eqid 2737 |
. . . 4
⊢ ;24 = ;24 |
| 106 | 21 | dec0h 12755 |
. . . 4
⊢ 5 = ;05 |
| 107 | 2, 1 | deccl 12748 |
. . . 4
⊢ ;13 ∈
ℕ0 |
| 108 | | eqid 2737 |
. . . . 5
⊢ ;13 = ;13 |
| 109 | 44 | addlidi 11449 |
. . . . . 6
⊢ (0 + 5) =
5 |
| 110 | 109, 106 | eqtri 2765 |
. . . . 5
⊢ (0 + 5) =
;05 |
| 111 | 16 | oveq1i 7441 |
. . . . . 6
⊢ ((3
· 2) + 5) = (6 + 5) |
| 112 | | 6p5e11 12806 |
. . . . . 6
⊢ (6 + 5) =
;11 |
| 113 | 111, 112 | eqtri 2765 |
. . . . 5
⊢ ((3
· 2) + 5) = ;11 |
| 114 | 2, 1, 24, 21, 108, 110, 25, 2, 2, 82, 113 | decmac 12785 |
. . . 4
⊢ ((;13 · 2) + (0 + 5)) = ;31 |
| 115 | | 4cn 12351 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
| 116 | 115 | mullidi 11266 |
. . . . . . 7
⊢ (1
· 4) = 4 |
| 117 | 116, 30 | oveq12i 7443 |
. . . . . 6
⊢ ((1
· 4) + (0 + 1)) = (4 + 1) |
| 118 | | 4p1e5 12412 |
. . . . . 6
⊢ (4 + 1) =
5 |
| 119 | 117, 118 | eqtri 2765 |
. . . . 5
⊢ ((1
· 4) + (0 + 1)) = 5 |
| 120 | | 4t3e12 12831 |
. . . . . . 7
⊢ (4
· 3) = ;12 |
| 121 | 115, 33, 120 | mulcomli 11270 |
. . . . . 6
⊢ (3
· 4) = ;12 |
| 122 | 44, 79, 47 | addcomli 11453 |
. . . . . 6
⊢ (2 + 5) =
7 |
| 123 | 2, 25, 21, 121, 122 | decaddi 12793 |
. . . . 5
⊢ ((3
· 4) + 5) = ;17 |
| 124 | 2, 1, 24, 21, 108, 106, 7, 8, 2, 119, 123 | decmac 12785 |
. . . 4
⊢ ((;13 · 4) + 5) = ;57 |
| 125 | 25, 7, 24, 21, 105, 106, 107, 8, 21, 114, 124 | decma2c 12786 |
. . 3
⊢ ((;13 · ;24) + 5) = ;;317 |
| 126 | | 5lt10 12868 |
. . . 4
⊢ 5 <
;10 |
| 127 | 13, 1, 21, 126 | declti 12771 |
. . 3
⊢ 5 <
;13 |
| 128 | 102, 103,
104, 125, 127 | ndvdsi 16449 |
. 2
⊢ ¬
;13 ∥ ;;317 |
| 129 | 2, 4 | decnncl 12753 |
. . 3
⊢ ;17 ∈ ℕ |
| 130 | 2, 6 | deccl 12748 |
. . 3
⊢ ;18 ∈
ℕ0 |
| 131 | | eqid 2737 |
. . . 4
⊢ ;18 = ;18 |
| 132 | 2, 8 | deccl 12748 |
. . . 4
⊢ ;17 ∈
ℕ0 |
| 133 | | eqid 2737 |
. . . . 5
⊢ ;17 = ;17 |
| 134 | | 3p1e4 12411 |
. . . . . . 7
⊢ (3 + 1) =
4 |
| 135 | 33, 29, 134 | addcomli 11453 |
. . . . . 6
⊢ (1 + 3) =
4 |
| 136 | 24, 2, 2, 1, 31, 108, 30, 135 | decadd 12787 |
. . . . 5
⊢ (1 +
;13) = ;14 |
| 137 | 29 | mulridi 11265 |
. . . . . . 7
⊢ (1
· 1) = 1 |
| 138 | | 1p1e2 12391 |
. . . . . . 7
⊢ (1 + 1) =
2 |
| 139 | 137, 138 | oveq12i 7443 |
. . . . . 6
⊢ ((1
· 1) + (1 + 1)) = (1 + 2) |
| 140 | | 1p2e3 12409 |
. . . . . 6
⊢ (1 + 2) =
3 |
| 141 | 139, 140 | eqtri 2765 |
. . . . 5
⊢ ((1
· 1) + (1 + 1)) = 3 |
| 142 | | 7cn 12360 |
. . . . . . . 8
⊢ 7 ∈
ℂ |
| 143 | 142 | mulridi 11265 |
. . . . . . 7
⊢ (7
· 1) = 7 |
| 144 | 143 | oveq1i 7441 |
. . . . . 6
⊢ ((7
· 1) + 4) = (7 + 4) |
| 145 | | 7p4e11 12809 |
. . . . . 6
⊢ (7 + 4) =
;11 |
| 146 | 144, 145 | eqtri 2765 |
. . . . 5
⊢ ((7
· 1) + 4) = ;11 |
| 147 | 2, 8, 2, 7, 133, 136, 2, 2, 2, 141, 146 | decmac 12785 |
. . . 4
⊢ ((;17 · 1) + (1 + ;13)) = ;31 |
| 148 | 89, 109 | oveq12i 7443 |
. . . . . 6
⊢ ((1
· 8) + (0 + 5)) = (8 + 5) |
| 149 | | 8p5e13 12816 |
. . . . . 6
⊢ (8 + 5) =
;13 |
| 150 | 148, 149 | eqtri 2765 |
. . . . 5
⊢ ((1
· 8) + (0 + 5)) = ;13 |
| 151 | | 6nn0 12547 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
| 152 | | 6p1e7 12414 |
. . . . . 6
⊢ (6 + 1) =
7 |
| 153 | | 8t7e56 12853 |
. . . . . . 7
⊢ (8
· 7) = ;56 |
| 154 | 88, 142, 153 | mulcomli 11270 |
. . . . . 6
⊢ (7
· 8) = ;56 |
| 155 | 21, 151, 152, 154 | decsuc 12764 |
. . . . 5
⊢ ((7
· 8) + 1) = ;57 |
| 156 | 2, 8, 24, 2, 133, 31, 6, 8, 21, 150, 155 | decmac 12785 |
. . . 4
⊢ ((;17 · 8) + 1) = ;;137 |
| 157 | 2, 6, 2, 2, 131, 75, 132, 8, 107, 147, 156 | decma2c 12786 |
. . 3
⊢ ((;17 · ;18) + ;11) = ;;317 |
| 158 | | 1lt7 12457 |
. . . 4
⊢ 1 <
7 |
| 159 | 2, 2, 4, 158 | declt 12761 |
. . 3
⊢ ;11 < ;17 |
| 160 | 129, 130,
68, 157, 159 | ndvdsi 16449 |
. 2
⊢ ¬
;17 ∥ ;;317 |
| 161 | 2, 70 | decnncl 12753 |
. . 3
⊢ ;19 ∈ ℕ |
| 162 | 2, 151 | deccl 12748 |
. . 3
⊢ ;16 ∈
ℕ0 |
| 163 | | eqid 2737 |
. . . 4
⊢ ;16 = ;16 |
| 164 | 2, 71 | deccl 12748 |
. . . 4
⊢ ;19 ∈
ℕ0 |
| 165 | | eqid 2737 |
. . . . 5
⊢ ;19 = ;19 |
| 166 | 24, 2, 2, 2, 31, 75, 30, 138 | decadd 12787 |
. . . . 5
⊢ (1 +
;11) = ;12 |
| 167 | 76 | mulridi 11265 |
. . . . . . 7
⊢ (9
· 1) = 9 |
| 168 | 167 | oveq1i 7441 |
. . . . . 6
⊢ ((9
· 1) + 2) = (9 + 2) |
| 169 | 168, 84 | eqtri 2765 |
. . . . 5
⊢ ((9
· 1) + 2) = ;11 |
| 170 | 2, 71, 2, 25, 165, 166, 2, 2, 2, 141, 169 | decmac 12785 |
. . . 4
⊢ ((;19 · 1) + (1 + ;11)) = ;31 |
| 171 | 1 | dec0h 12755 |
. . . . 5
⊢ 3 = ;03 |
| 172 | | 6cn 12357 |
. . . . . . . 8
⊢ 6 ∈
ℂ |
| 173 | 172 | mullidi 11266 |
. . . . . . 7
⊢ (1
· 6) = 6 |
| 174 | 173, 109 | oveq12i 7443 |
. . . . . 6
⊢ ((1
· 6) + (0 + 5)) = (6 + 5) |
| 175 | 174, 112 | eqtri 2765 |
. . . . 5
⊢ ((1
· 6) + (0 + 5)) = ;11 |
| 176 | | 9t6e54 12859 |
. . . . . 6
⊢ (9
· 6) = ;54 |
| 177 | | 4p3e7 12420 |
. . . . . 6
⊢ (4 + 3) =
7 |
| 178 | 21, 7, 1, 176, 177 | decaddi 12793 |
. . . . 5
⊢ ((9
· 6) + 3) = ;57 |
| 179 | 2, 71, 24, 1, 165, 171, 151, 8, 21, 175, 178 | decmac 12785 |
. . . 4
⊢ ((;19 · 6) + 3) = ;;117 |
| 180 | 2, 151, 2, 1, 163, 108, 164, 8, 74, 170, 179 | decma2c 12786 |
. . 3
⊢ ((;19 · ;16) + ;13) = ;;317 |
| 181 | | 3lt9 12470 |
. . . 4
⊢ 3 <
9 |
| 182 | 2, 1, 70, 181 | declt 12761 |
. . 3
⊢ ;13 < ;19 |
| 183 | 161, 162,
102, 180, 182 | ndvdsi 16449 |
. 2
⊢ ¬
;19 ∥ ;;317 |
| 184 | 25, 19 | decnncl 12753 |
. . 3
⊢ ;23 ∈ ℕ |
| 185 | 102 | nnnn0i 12534 |
. . 3
⊢ ;13 ∈
ℕ0 |
| 186 | | 8nn 12361 |
. . . 4
⊢ 8 ∈
ℕ |
| 187 | 2, 186 | decnncl 12753 |
. . 3
⊢ ;18 ∈ ℕ |
| 188 | 25, 1 | deccl 12748 |
. . . 4
⊢ ;23 ∈
ℕ0 |
| 189 | | eqid 2737 |
. . . . 5
⊢ ;23 = ;23 |
| 190 | | 7p1e8 12415 |
. . . . . . 7
⊢ (7 + 1) =
8 |
| 191 | 142, 29, 190 | addcomli 11453 |
. . . . . 6
⊢ (1 + 7) =
8 |
| 192 | 6 | dec0h 12755 |
. . . . . 6
⊢ 8 = ;08 |
| 193 | 191, 192 | eqtri 2765 |
. . . . 5
⊢ (1 + 7) =
;08 |
| 194 | 79 | mulridi 11265 |
. . . . . . 7
⊢ (2
· 1) = 2 |
| 195 | 194, 30 | oveq12i 7443 |
. . . . . 6
⊢ ((2
· 1) + (0 + 1)) = (2 + 1) |
| 196 | 195, 59 | eqtri 2765 |
. . . . 5
⊢ ((2
· 1) + (0 + 1)) = 3 |
| 197 | 34 | oveq1i 7441 |
. . . . . 6
⊢ ((3
· 1) + 8) = (3 + 8) |
| 198 | 88, 33, 60 | addcomli 11453 |
. . . . . 6
⊢ (3 + 8) =
;11 |
| 199 | 197, 198 | eqtri 2765 |
. . . . 5
⊢ ((3
· 1) + 8) = ;11 |
| 200 | 25, 1, 24, 6, 189, 193, 2, 2, 2, 196, 199 | decmac 12785 |
. . . 4
⊢ ((;23 · 1) + (1 + 7)) = ;31 |
| 201 | 33, 79, 16 | mulcomli 11270 |
. . . . . . 7
⊢ (2
· 3) = 6 |
| 202 | 201, 30 | oveq12i 7443 |
. . . . . 6
⊢ ((2
· 3) + (0 + 1)) = (6 + 1) |
| 203 | 202, 152 | eqtri 2765 |
. . . . 5
⊢ ((2
· 3) + (0 + 1)) = 7 |
| 204 | | 3t3e9 12433 |
. . . . . . 7
⊢ (3
· 3) = 9 |
| 205 | 204 | oveq1i 7441 |
. . . . . 6
⊢ ((3
· 3) + 8) = (9 + 8) |
| 206 | 205, 94 | eqtri 2765 |
. . . . 5
⊢ ((3
· 3) + 8) = ;17 |
| 207 | 25, 1, 24, 6, 189, 192, 1, 8, 2, 203, 206 | decmac 12785 |
. . . 4
⊢ ((;23 · 3) + 8) = ;77 |
| 208 | 2, 1, 2, 6, 108, 131, 188, 8, 8, 200, 207 | decma2c 12786 |
. . 3
⊢ ((;23 · ;13) + ;18) = ;;317 |
| 209 | | 8lt10 12865 |
. . . 4
⊢ 8 <
;10 |
| 210 | | 1lt2 12437 |
. . . 4
⊢ 1 <
2 |
| 211 | 2, 25, 6, 1, 209, 210 | decltc 12762 |
. . 3
⊢ ;18 < ;23 |
| 212 | 184, 185,
187, 208, 211 | ndvdsi 16449 |
. 2
⊢ ¬
;23 ∥ ;;317 |
| 213 | 5, 12, 15, 18, 51, 53, 67, 101, 128, 160, 183, 212 | prmlem2 17157 |
1
⊢ ;;317 ∈ ℙ |