Proof of Theorem 163prm
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1nn0 12544 | . . . 4
⊢ 1 ∈
ℕ0 | 
| 2 |  | 6nn0 12549 | . . . 4
⊢ 6 ∈
ℕ0 | 
| 3 | 1, 2 | deccl 12750 | . . 3
⊢ ;16 ∈
ℕ0 | 
| 4 |  | 3nn 12346 | . . 3
⊢ 3 ∈
ℕ | 
| 5 | 3, 4 | decnncl 12755 | . 2
⊢ ;;163 ∈ ℕ | 
| 6 |  | 8nn0 12551 | . . 3
⊢ 8 ∈
ℕ0 | 
| 7 |  | 4nn0 12547 | . . 3
⊢ 4 ∈
ℕ0 | 
| 8 |  | 3nn0 12546 | . . 3
⊢ 3 ∈
ℕ0 | 
| 9 |  | 1lt8 12465 | . . 3
⊢ 1 <
8 | 
| 10 |  | 6lt10 12869 | . . 3
⊢ 6 <
;10 | 
| 11 |  | 3lt10 12872 | . . 3
⊢ 3 <
;10 | 
| 12 | 1, 6, 2, 7, 8, 1, 9, 10, 11 | 3decltc 12768 | . 2
⊢ ;;163 < ;;841 | 
| 13 |  | 6nn 12356 | . . . 4
⊢ 6 ∈
ℕ | 
| 14 | 1, 13 | decnncl 12755 | . . 3
⊢ ;16 ∈ ℕ | 
| 15 |  | 1lt10 12874 | . . 3
⊢ 1 <
;10 | 
| 16 | 14, 8, 1, 15 | declti 12773 | . 2
⊢ 1 <
;;163 | 
| 17 |  | 2cn 12342 | . . . 4
⊢ 2 ∈
ℂ | 
| 18 | 17 | mullidi 11267 | . . 3
⊢ (1
· 2) = 2 | 
| 19 |  | df-3 12331 | . . 3
⊢ 3 = (2 +
1) | 
| 20 | 3, 1, 18, 19 | dec2dvds 17102 | . 2
⊢  ¬ 2
∥ ;;163 | 
| 21 |  | 5nn0 12548 | . . . 4
⊢ 5 ∈
ℕ0 | 
| 22 | 21, 7 | deccl 12750 | . . 3
⊢ ;54 ∈
ℕ0 | 
| 23 |  | 1nn 12278 | . . 3
⊢ 1 ∈
ℕ | 
| 24 |  | 0nn0 12543 | . . . 4
⊢ 0 ∈
ℕ0 | 
| 25 |  | eqid 2736 | . . . 4
⊢ ;54 = ;54 | 
| 26 | 1 | dec0h 12757 | . . . 4
⊢ 1 = ;01 | 
| 27 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 28 | 27 | addlidi 11450 | . . . . . 6
⊢ (0 + 1) =
1 | 
| 29 | 28 | oveq2i 7443 | . . . . 5
⊢ ((3
· 5) + (0 + 1)) = ((3 · 5) + 1) | 
| 30 |  | 5p1e6 12414 | . . . . . 6
⊢ (5 + 1) =
6 | 
| 31 |  | 5cn 12355 | . . . . . . 7
⊢ 5 ∈
ℂ | 
| 32 |  | 3cn 12348 | . . . . . . 7
⊢ 3 ∈
ℂ | 
| 33 |  | 5t3e15 12836 | . . . . . . 7
⊢ (5
· 3) = ;15 | 
| 34 | 31, 32, 33 | mulcomli 11271 | . . . . . 6
⊢ (3
· 5) = ;15 | 
| 35 | 1, 21, 30, 34 | decsuc 12766 | . . . . 5
⊢ ((3
· 5) + 1) = ;16 | 
| 36 | 29, 35 | eqtri 2764 | . . . 4
⊢ ((3
· 5) + (0 + 1)) = ;16 | 
| 37 |  | 2nn0 12545 | . . . . 5
⊢ 2 ∈
ℕ0 | 
| 38 |  | 2p1e3 12409 | . . . . 5
⊢ (2 + 1) =
3 | 
| 39 |  | 4cn 12352 | . . . . . 6
⊢ 4 ∈
ℂ | 
| 40 |  | 4t3e12 12833 | . . . . . 6
⊢ (4
· 3) = ;12 | 
| 41 | 39, 32, 40 | mulcomli 11271 | . . . . 5
⊢ (3
· 4) = ;12 | 
| 42 | 1, 37, 38, 41 | decsuc 12766 | . . . 4
⊢ ((3
· 4) + 1) = ;13 | 
| 43 | 21, 7, 24, 1, 25, 26, 8, 8, 1,
36, 42 | decma2c 12788 | . . 3
⊢ ((3
· ;54) + 1) = ;;163 | 
| 44 |  | 1lt3 12440 | . . 3
⊢ 1 <
3 | 
| 45 | 4, 22, 23, 43, 44 | ndvdsi 16450 | . 2
⊢  ¬ 3
∥ ;;163 | 
| 46 |  | 3lt5 12445 | . . 3
⊢ 3 <
5 | 
| 47 | 3, 4, 46 | dec5dvds 17103 | . 2
⊢  ¬ 5
∥ ;;163 | 
| 48 |  | 7nn 12359 | . . 3
⊢ 7 ∈
ℕ | 
| 49 | 37, 8 | deccl 12750 | . . 3
⊢ ;23 ∈
ℕ0 | 
| 50 |  | 2nn 12340 | . . 3
⊢ 2 ∈
ℕ | 
| 51 |  | eqid 2736 | . . . 4
⊢ ;23 = ;23 | 
| 52 | 37 | dec0h 12757 | . . . 4
⊢ 2 = ;02 | 
| 53 |  | 7nn0 12550 | . . . 4
⊢ 7 ∈
ℕ0 | 
| 54 | 17 | addlidi 11450 | . . . . . 6
⊢ (0 + 2) =
2 | 
| 55 | 54 | oveq2i 7443 | . . . . 5
⊢ ((7
· 2) + (0 + 2)) = ((7 · 2) + 2) | 
| 56 |  | 7t2e14 12844 | . . . . . 6
⊢ (7
· 2) = ;14 | 
| 57 |  | 4p2e6 12420 | . . . . . 6
⊢ (4 + 2) =
6 | 
| 58 | 1, 7, 37, 56, 57 | decaddi 12795 | . . . . 5
⊢ ((7
· 2) + 2) = ;16 | 
| 59 | 55, 58 | eqtri 2764 | . . . 4
⊢ ((7
· 2) + (0 + 2)) = ;16 | 
| 60 |  | 7t3e21 12845 | . . . . 5
⊢ (7
· 3) = ;21 | 
| 61 |  | 1p2e3 12410 | . . . . 5
⊢ (1 + 2) =
3 | 
| 62 | 37, 1, 37, 60, 61 | decaddi 12795 | . . . 4
⊢ ((7
· 3) + 2) = ;23 | 
| 63 | 37, 8, 24, 37, 51, 52, 53, 8, 37, 59, 62 | decma2c 12788 | . . 3
⊢ ((7
· ;23) + 2) = ;;163 | 
| 64 |  | 2lt7 12457 | . . 3
⊢ 2 <
7 | 
| 65 | 48, 49, 50, 63, 64 | ndvdsi 16450 | . 2
⊢  ¬ 7
∥ ;;163 | 
| 66 | 1, 23 | decnncl 12755 | . . 3
⊢ ;11 ∈ ℕ | 
| 67 | 1, 7 | deccl 12750 | . . 3
⊢ ;14 ∈
ℕ0 | 
| 68 |  | 9nn 12365 | . . 3
⊢ 9 ∈
ℕ | 
| 69 |  | 9nn0 12552 | . . . 4
⊢ 9 ∈
ℕ0 | 
| 70 |  | eqid 2736 | . . . 4
⊢ ;14 = ;14 | 
| 71 | 69 | dec0h 12757 | . . . 4
⊢ 9 = ;09 | 
| 72 | 1, 1 | deccl 12750 | . . . 4
⊢ ;11 ∈
ℕ0 | 
| 73 | 31 | addlidi 11450 | . . . . . 6
⊢ (0 + 5) =
5 | 
| 74 | 73 | oveq2i 7443 | . . . . 5
⊢ ((;11 · 1) + (0 + 5)) = ((;11 · 1) + 5) | 
| 75 | 66 | nncni 12277 | . . . . . . 7
⊢ ;11 ∈ ℂ | 
| 76 | 75 | mulridi 11266 | . . . . . 6
⊢ (;11 · 1) = ;11 | 
| 77 | 31, 27, 30 | addcomli 11454 | . . . . . 6
⊢ (1 + 5) =
6 | 
| 78 | 1, 1, 21, 76, 77 | decaddi 12795 | . . . . 5
⊢ ((;11 · 1) + 5) = ;16 | 
| 79 | 74, 78 | eqtri 2764 | . . . 4
⊢ ((;11 · 1) + (0 + 5)) = ;16 | 
| 80 |  | eqid 2736 | . . . . 5
⊢ ;11 = ;11 | 
| 81 | 39 | mullidi 11267 | . . . . . . 7
⊢ (1
· 4) = 4 | 
| 82 | 81, 28 | oveq12i 7444 | . . . . . 6
⊢ ((1
· 4) + (0 + 1)) = (4 + 1) | 
| 83 |  | 4p1e5 12413 | . . . . . 6
⊢ (4 + 1) =
5 | 
| 84 | 82, 83 | eqtri 2764 | . . . . 5
⊢ ((1
· 4) + (0 + 1)) = 5 | 
| 85 | 81 | oveq1i 7442 | . . . . . 6
⊢ ((1
· 4) + 9) = (4 + 9) | 
| 86 |  | 9cn 12367 | . . . . . . 7
⊢ 9 ∈
ℂ | 
| 87 |  | 9p4e13 12824 | . . . . . . 7
⊢ (9 + 4) =
;13 | 
| 88 | 86, 39, 87 | addcomli 11454 | . . . . . 6
⊢ (4 + 9) =
;13 | 
| 89 | 85, 88 | eqtri 2764 | . . . . 5
⊢ ((1
· 4) + 9) = ;13 | 
| 90 | 1, 1, 24, 69, 80, 71, 7, 8, 1,
84, 89 | decmac 12787 | . . . 4
⊢ ((;11 · 4) + 9) = ;53 | 
| 91 | 1, 7, 24, 69, 70, 71, 72, 8, 21, 79, 90 | decma2c 12788 | . . 3
⊢ ((;11 · ;14) + 9) = ;;163 | 
| 92 |  | 9lt10 12866 | . . . 4
⊢ 9 <
;10 | 
| 93 | 23, 1, 69, 92 | declti 12773 | . . 3
⊢ 9 <
;11 | 
| 94 | 66, 67, 68, 91, 93 | ndvdsi 16450 | . 2
⊢  ¬
;11 ∥ ;;163 | 
| 95 | 1, 4 | decnncl 12755 | . . 3
⊢ ;13 ∈ ℕ | 
| 96 | 1, 37 | deccl 12750 | . . 3
⊢ ;12 ∈
ℕ0 | 
| 97 |  | eqid 2736 | . . . 4
⊢ ;12 = ;12 | 
| 98 | 53 | dec0h 12757 | . . . 4
⊢ 7 = ;07 | 
| 99 | 1, 8 | deccl 12750 | . . . 4
⊢ ;13 ∈
ℕ0 | 
| 100 |  | eqid 2736 | . . . . 5
⊢ ;13 = ;13 | 
| 101 | 32 | addlidi 11450 | . . . . . 6
⊢ (0 + 3) =
3 | 
| 102 | 8 | dec0h 12757 | . . . . . 6
⊢ 3 = ;03 | 
| 103 | 101, 102 | eqtri 2764 | . . . . 5
⊢ (0 + 3) =
;03 | 
| 104 | 27 | mulridi 11266 | . . . . . . 7
⊢ (1
· 1) = 1 | 
| 105 |  | 00id 11437 | . . . . . . 7
⊢ (0 + 0) =
0 | 
| 106 | 104, 105 | oveq12i 7444 | . . . . . 6
⊢ ((1
· 1) + (0 + 0)) = (1 + 0) | 
| 107 | 27 | addridi 11449 | . . . . . 6
⊢ (1 + 0) =
1 | 
| 108 | 106, 107 | eqtri 2764 | . . . . 5
⊢ ((1
· 1) + (0 + 0)) = 1 | 
| 109 | 32 | mulridi 11266 | . . . . . . . 8
⊢ (3
· 1) = 3 | 
| 110 | 109 | oveq1i 7442 | . . . . . . 7
⊢ ((3
· 1) + 3) = (3 + 3) | 
| 111 |  | 3p3e6 12419 | . . . . . . 7
⊢ (3 + 3) =
6 | 
| 112 | 110, 111 | eqtri 2764 | . . . . . 6
⊢ ((3
· 1) + 3) = 6 | 
| 113 | 2 | dec0h 12757 | . . . . . 6
⊢ 6 = ;06 | 
| 114 | 112, 113 | eqtri 2764 | . . . . 5
⊢ ((3
· 1) + 3) = ;06 | 
| 115 | 1, 8, 24, 8, 100, 103, 1, 2, 24, 108, 114 | decmac 12787 | . . . 4
⊢ ((;13 · 1) + (0 + 3)) = ;16 | 
| 116 | 18, 28 | oveq12i 7444 | . . . . . 6
⊢ ((1
· 2) + (0 + 1)) = (2 + 1) | 
| 117 | 116, 38 | eqtri 2764 | . . . . 5
⊢ ((1
· 2) + (0 + 1)) = 3 | 
| 118 |  | 3t2e6 12433 | . . . . . . 7
⊢ (3
· 2) = 6 | 
| 119 | 118 | oveq1i 7442 | . . . . . 6
⊢ ((3
· 2) + 7) = (6 + 7) | 
| 120 |  | 7cn 12361 | . . . . . . 7
⊢ 7 ∈
ℂ | 
| 121 |  | 6cn 12358 | . . . . . . 7
⊢ 6 ∈
ℂ | 
| 122 |  | 7p6e13 12813 | . . . . . . 7
⊢ (7 + 6) =
;13 | 
| 123 | 120, 121,
122 | addcomli 11454 | . . . . . 6
⊢ (6 + 7) =
;13 | 
| 124 | 119, 123 | eqtri 2764 | . . . . 5
⊢ ((3
· 2) + 7) = ;13 | 
| 125 | 1, 8, 24, 53, 100, 98, 37, 8, 1, 117, 124 | decmac 12787 | . . . 4
⊢ ((;13 · 2) + 7) = ;33 | 
| 126 | 1, 37, 24, 53, 97, 98, 99, 8, 8, 115, 125 | decma2c 12788 | . . 3
⊢ ((;13 · ;12) + 7) = ;;163 | 
| 127 |  | 7lt10 12868 | . . . 4
⊢ 7 <
;10 | 
| 128 | 23, 8, 53, 127 | declti 12773 | . . 3
⊢ 7 <
;13 | 
| 129 | 95, 96, 48, 126, 128 | ndvdsi 16450 | . 2
⊢  ¬
;13 ∥ ;;163 | 
| 130 | 1, 48 | decnncl 12755 | . . 3
⊢ ;17 ∈ ℕ | 
| 131 |  | 10nn 12751 | . . 3
⊢ ;10 ∈ ℕ | 
| 132 |  | eqid 2736 | . . . 4
⊢ ;17 = ;17 | 
| 133 |  | eqid 2736 | . . . 4
⊢ ;10 = ;10 | 
| 134 | 86 | mullidi 11267 | . . . . . 6
⊢ (1
· 9) = 9 | 
| 135 |  | 6p1e7 12415 | . . . . . . 7
⊢ (6 + 1) =
7 | 
| 136 | 121, 27, 135 | addcomli 11454 | . . . . . 6
⊢ (1 + 6) =
7 | 
| 137 | 134, 136 | oveq12i 7444 | . . . . 5
⊢ ((1
· 9) + (1 + 6)) = (9 + 7) | 
| 138 |  | 9p7e16 12827 | . . . . 5
⊢ (9 + 7) =
;16 | 
| 139 | 137, 138 | eqtri 2764 | . . . 4
⊢ ((1
· 9) + (1 + 6)) = ;16 | 
| 140 |  | 9t7e63 12862 | . . . . . . 7
⊢ (9
· 7) = ;63 | 
| 141 | 86, 120, 140 | mulcomli 11271 | . . . . . 6
⊢ (7
· 9) = ;63 | 
| 142 | 141 | oveq1i 7442 | . . . . 5
⊢ ((7
· 9) + 0) = (;63 +
0) | 
| 143 | 2, 8 | deccl 12750 | . . . . . . 7
⊢ ;63 ∈
ℕ0 | 
| 144 | 143 | nn0cni 12540 | . . . . . 6
⊢ ;63 ∈ ℂ | 
| 145 | 144 | addridi 11449 | . . . . 5
⊢ (;63 + 0) = ;63 | 
| 146 | 142, 145 | eqtri 2764 | . . . 4
⊢ ((7
· 9) + 0) = ;63 | 
| 147 | 1, 53, 1, 24, 132, 133, 69, 8, 2, 139, 146 | decmac 12787 | . . 3
⊢ ((;17 · 9) + ;10) = ;;163 | 
| 148 |  | 7pos 12378 | . . . 4
⊢ 0 <
7 | 
| 149 | 1, 24, 48, 148 | declt 12763 | . . 3
⊢ ;10 < ;17 | 
| 150 | 130, 69, 131, 147, 149 | ndvdsi 16450 | . 2
⊢  ¬
;17 ∥ ;;163 | 
| 151 | 1, 68 | decnncl 12755 | . . 3
⊢ ;19 ∈ ℕ | 
| 152 |  | eqid 2736 | . . . 4
⊢ ;19 = ;19 | 
| 153 |  | 8cn 12364 | . . . . . . 7
⊢ 8 ∈
ℂ | 
| 154 | 153 | mullidi 11267 | . . . . . 6
⊢ (1
· 8) = 8 | 
| 155 |  | 7p1e8 12416 | . . . . . . 7
⊢ (7 + 1) =
8 | 
| 156 | 120, 27, 155 | addcomli 11454 | . . . . . 6
⊢ (1 + 7) =
8 | 
| 157 | 154, 156 | oveq12i 7444 | . . . . 5
⊢ ((1
· 8) + (1 + 7)) = (8 + 8) | 
| 158 |  | 8p8e16 12821 | . . . . 5
⊢ (8 + 8) =
;16 | 
| 159 | 157, 158 | eqtri 2764 | . . . 4
⊢ ((1
· 8) + (1 + 7)) = ;16 | 
| 160 |  | 9t8e72 12863 | . . . . 5
⊢ (9
· 8) = ;72 | 
| 161 | 53, 37, 38, 160 | decsuc 12766 | . . . 4
⊢ ((9
· 8) + 1) = ;73 | 
| 162 | 1, 69, 1, 1, 152, 80, 6, 8, 53, 159, 161 | decmac 12787 | . . 3
⊢ ((;19 · 8) + ;11) = ;;163 | 
| 163 |  | 1lt9 12473 | . . . 4
⊢ 1 <
9 | 
| 164 | 1, 1, 68, 163 | declt 12763 | . . 3
⊢ ;11 < ;19 | 
| 165 | 151, 6, 66, 162, 164 | ndvdsi 16450 | . 2
⊢  ¬
;19 ∥ ;;163 | 
| 166 | 37, 4 | decnncl 12755 | . . 3
⊢ ;23 ∈ ℕ | 
| 167 | 120, 17, 56 | mulcomli 11271 | . . . . 5
⊢ (2
· 7) = ;14 | 
| 168 | 1, 7, 37, 167, 57 | decaddi 12795 | . . . 4
⊢ ((2
· 7) + 2) = ;16 | 
| 169 | 120, 32, 60 | mulcomli 11271 | . . . . 5
⊢ (3
· 7) = ;21 | 
| 170 | 37, 1, 37, 169, 61 | decaddi 12795 | . . . 4
⊢ ((3
· 7) + 2) = ;23 | 
| 171 | 37, 8, 37, 51, 53, 8, 37, 168, 170 | decrmac 12793 | . . 3
⊢ ((;23 · 7) + 2) = ;;163 | 
| 172 |  | 2lt10 12873 | . . . 4
⊢ 2 <
;10 | 
| 173 | 50, 8, 37, 172 | declti 12773 | . . 3
⊢ 2 <
;23 | 
| 174 | 166, 53, 50, 171, 173 | ndvdsi 16450 | . 2
⊢  ¬
;23 ∥ ;;163 | 
| 175 | 5, 12, 16, 20, 45, 47, 65, 94, 129, 150, 165, 174 | prmlem2 17158 | 1
⊢ ;;163 ∈ ℙ |