Proof of Theorem 1259lem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2nn 12340 | . 2
⊢ 2 ∈
ℕ | 
| 2 |  | 6nn0 12549 | . . . 4
⊢ 6 ∈
ℕ0 | 
| 3 |  | 2nn0 12545 | . . . 4
⊢ 2 ∈
ℕ0 | 
| 4 | 2, 3 | deccl 12750 | . . 3
⊢ ;62 ∈
ℕ0 | 
| 5 |  | 9nn0 12552 | . . 3
⊢ 9 ∈
ℕ0 | 
| 6 | 4, 5 | deccl 12750 | . 2
⊢ ;;629 ∈ ℕ0 | 
| 7 |  | 0z 12626 | . 2
⊢ 0 ∈
ℤ | 
| 8 |  | 1nn 12278 | . 2
⊢ 1 ∈
ℕ | 
| 9 |  | 1nn0 12544 | . 2
⊢ 1 ∈
ℕ0 | 
| 10 | 9, 3 | deccl 12750 | . . . . . . 7
⊢ ;12 ∈
ℕ0 | 
| 11 |  | 5nn0 12548 | . . . . . . 7
⊢ 5 ∈
ℕ0 | 
| 12 | 10, 11 | deccl 12750 | . . . . . 6
⊢ ;;125 ∈ ℕ0 | 
| 13 |  | 8nn0 12551 | . . . . . 6
⊢ 8 ∈
ℕ0 | 
| 14 | 12, 13 | deccl 12750 | . . . . 5
⊢ ;;;1258
∈ ℕ0 | 
| 15 | 14 | nn0cni 12540 | . . . 4
⊢ ;;;1258
∈ ℂ | 
| 16 |  | ax-1cn 11214 | . . . 4
⊢ 1 ∈
ℂ | 
| 17 |  | 1259prm.1 | . . . . 5
⊢ 𝑁 = ;;;1259 | 
| 18 |  | 8p1e9 12417 | . . . . . 6
⊢ (8 + 1) =
9 | 
| 19 |  | eqid 2736 | . . . . . 6
⊢ ;;;1258 =
;;;1258 | 
| 20 | 12, 13, 18, 19 | decsuc 12766 | . . . . 5
⊢ (;;;1258 +
1) = ;;;1259 | 
| 21 | 17, 20 | eqtr4i 2767 | . . . 4
⊢ 𝑁 = (;;;1258 + 1) | 
| 22 | 15, 16, 21 | mvrraddi 11526 | . . 3
⊢ (𝑁 − 1) = ;;;1258 | 
| 23 | 22, 14 | eqeltri 2836 | . 2
⊢ (𝑁 − 1) ∈
ℕ0 | 
| 24 |  | 9nn 12365 | . . . . 5
⊢ 9 ∈
ℕ | 
| 25 | 12, 24 | decnncl 12755 | . . . 4
⊢ ;;;1259
∈ ℕ | 
| 26 | 17, 25 | eqeltri 2836 | . . 3
⊢ 𝑁 ∈ ℕ | 
| 27 | 2, 9 | deccl 12750 | . . . 4
⊢ ;61 ∈
ℕ0 | 
| 28 | 27, 3 | deccl 12750 | . . 3
⊢ ;;612 ∈ ℕ0 | 
| 29 |  | 3nn0 12546 | . . . . 5
⊢ 3 ∈
ℕ0 | 
| 30 |  | 4nn0 12547 | . . . . 5
⊢ 4 ∈
ℕ0 | 
| 31 | 29, 30 | deccl 12750 | . . . 4
⊢ ;34 ∈
ℕ0 | 
| 32 | 31 | nn0zi 12644 | . . 3
⊢ ;34 ∈ ℤ | 
| 33 | 29, 3 | deccl 12750 | . . . 4
⊢ ;32 ∈
ℕ0 | 
| 34 | 33, 30 | deccl 12750 | . . 3
⊢ ;;324 ∈ ℕ0 | 
| 35 |  | 7nn0 12550 | . . . 4
⊢ 7 ∈
ℕ0 | 
| 36 | 9, 35 | deccl 12750 | . . 3
⊢ ;17 ∈
ℕ0 | 
| 37 | 9, 29 | deccl 12750 | . . . 4
⊢ ;13 ∈
ℕ0 | 
| 38 | 37, 2 | deccl 12750 | . . 3
⊢ ;;136 ∈ ℕ0 | 
| 39 |  | 0nn0 12543 | . . . . . 6
⊢ 0 ∈
ℕ0 | 
| 40 | 29, 39 | deccl 12750 | . . . . 5
⊢ ;30 ∈
ℕ0 | 
| 41 | 40, 2 | deccl 12750 | . . . 4
⊢ ;;306 ∈ ℕ0 | 
| 42 |  | 8nn 12362 | . . . . 5
⊢ 8 ∈
ℕ | 
| 43 | 9, 42 | decnncl 12755 | . . . 4
⊢ ;18 ∈ ℕ | 
| 44 | 10, 30 | deccl 12750 | . . . . 5
⊢ ;;124 ∈ ℕ0 | 
| 45 | 44, 9 | deccl 12750 | . . . 4
⊢ ;;;1241
∈ ℕ0 | 
| 46 | 9, 11 | deccl 12750 | . . . . . 6
⊢ ;15 ∈
ℕ0 | 
| 47 | 46, 29 | deccl 12750 | . . . . 5
⊢ ;;153 ∈ ℕ0 | 
| 48 |  | 1z 12649 | . . . . 5
⊢ 1 ∈
ℤ | 
| 49 | 11, 39 | deccl 12750 | . . . . 5
⊢ ;50 ∈
ℕ0 | 
| 50 | 46, 3 | deccl 12750 | . . . . . 6
⊢ ;;152 ∈ ℕ0 | 
| 51 | 3, 11 | deccl 12750 | . . . . . 6
⊢ ;25 ∈
ℕ0 | 
| 52 | 35, 2 | deccl 12750 | . . . . . . 7
⊢ ;76 ∈
ℕ0 | 
| 53 | 17 | 1259lem3 17171 | . . . . . . 7
⊢
((2↑;76) mod 𝑁) = (5 mod 𝑁) | 
| 54 |  | eqid 2736 | . . . . . . . 8
⊢ ;76 = ;76 | 
| 55 |  | 4p1e5 12413 | . . . . . . . . 9
⊢ (4 + 1) =
5 | 
| 56 |  | 7cn 12361 | . . . . . . . . . 10
⊢ 7 ∈
ℂ | 
| 57 |  | 2cn 12342 | . . . . . . . . . 10
⊢ 2 ∈
ℂ | 
| 58 |  | 7t2e14 12844 | . . . . . . . . . 10
⊢ (7
· 2) = ;14 | 
| 59 | 56, 57, 58 | mulcomli 11271 | . . . . . . . . 9
⊢ (2
· 7) = ;14 | 
| 60 | 9, 30, 55, 59 | decsuc 12766 | . . . . . . . 8
⊢ ((2
· 7) + 1) = ;15 | 
| 61 |  | 6cn 12358 | . . . . . . . . 9
⊢ 6 ∈
ℂ | 
| 62 |  | 6t2e12 12839 | . . . . . . . . 9
⊢ (6
· 2) = ;12 | 
| 63 | 61, 57, 62 | mulcomli 11271 | . . . . . . . 8
⊢ (2
· 6) = ;12 | 
| 64 | 3, 35, 2, 54, 3, 9,
60, 63 | decmul2c 12801 | . . . . . . 7
⊢ (2
· ;76) = ;;152 | 
| 65 | 51 | nn0cni 12540 | . . . . . . . . 9
⊢ ;25 ∈ ℂ | 
| 66 | 65 | addlidi 11450 | . . . . . . . 8
⊢ (0 +
;25) = ;25 | 
| 67 | 26 | nncni 12277 | . . . . . . . . . 10
⊢ 𝑁 ∈ ℂ | 
| 68 | 67 | mul02i 11451 | . . . . . . . . 9
⊢ (0
· 𝑁) =
0 | 
| 69 | 68 | oveq1i 7442 | . . . . . . . 8
⊢ ((0
· 𝑁) + ;25) = (0 + ;25) | 
| 70 |  | 5t5e25 12838 | . . . . . . . 8
⊢ (5
· 5) = ;25 | 
| 71 | 66, 69, 70 | 3eqtr4i 2774 | . . . . . . 7
⊢ ((0
· 𝑁) + ;25) = (5 · 5) | 
| 72 | 26, 1, 52, 7, 11, 51, 53, 64, 71 | mod2xi 17108 | . . . . . 6
⊢
((2↑;;152) mod 𝑁) = (;25 mod 𝑁) | 
| 73 |  | 2p1e3 12409 | . . . . . . 7
⊢ (2 + 1) =
3 | 
| 74 |  | eqid 2736 | . . . . . . 7
⊢ ;;152 = ;;152 | 
| 75 | 46, 3, 73, 74 | decsuc 12766 | . . . . . 6
⊢ (;;152 + 1) = ;;153 | 
| 76 | 49 | nn0cni 12540 | . . . . . . . 8
⊢ ;50 ∈ ℂ | 
| 77 | 76 | addlidi 11450 | . . . . . . 7
⊢ (0 +
;50) = ;50 | 
| 78 | 68 | oveq1i 7442 | . . . . . . 7
⊢ ((0
· 𝑁) + ;50) = (0 + ;50) | 
| 79 |  | eqid 2736 | . . . . . . . 8
⊢ ;25 = ;25 | 
| 80 |  | 2t2e4 12431 | . . . . . . . . . 10
⊢ (2
· 2) = 4 | 
| 81 | 80 | oveq1i 7442 | . . . . . . . . 9
⊢ ((2
· 2) + 1) = (4 + 1) | 
| 82 | 81, 55 | eqtri 2764 | . . . . . . . 8
⊢ ((2
· 2) + 1) = 5 | 
| 83 |  | 5t2e10 12835 | . . . . . . . 8
⊢ (5
· 2) = ;10 | 
| 84 | 3, 3, 11, 79, 39, 9, 82, 83 | decmul1c 12800 | . . . . . . 7
⊢ (;25 · 2) = ;50 | 
| 85 | 77, 78, 84 | 3eqtr4i 2774 | . . . . . 6
⊢ ((0
· 𝑁) + ;50) = (;25 · 2) | 
| 86 | 26, 1, 50, 7, 51, 49, 72, 75, 85 | modxp1i 17109 | . . . . 5
⊢
((2↑;;153) mod 𝑁) = (;50 mod 𝑁) | 
| 87 |  | eqid 2736 | . . . . . 6
⊢ ;;153 = ;;153 | 
| 88 |  | eqid 2736 | . . . . . . . . 9
⊢ ;15 = ;15 | 
| 89 | 57 | mulridi 11266 | . . . . . . . . . . 11
⊢ (2
· 1) = 2 | 
| 90 | 89 | oveq1i 7442 | . . . . . . . . . 10
⊢ ((2
· 1) + 1) = (2 + 1) | 
| 91 | 90, 73 | eqtri 2764 | . . . . . . . . 9
⊢ ((2
· 1) + 1) = 3 | 
| 92 |  | 5cn 12355 | . . . . . . . . . 10
⊢ 5 ∈
ℂ | 
| 93 | 92, 57, 83 | mulcomli 11271 | . . . . . . . . 9
⊢ (2
· 5) = ;10 | 
| 94 | 3, 9, 11, 88, 39, 9, 91, 93 | decmul2c 12801 | . . . . . . . 8
⊢ (2
· ;15) = ;30 | 
| 95 | 94 | oveq1i 7442 | . . . . . . 7
⊢ ((2
· ;15) + 0) = (;30 + 0) | 
| 96 | 40 | nn0cni 12540 | . . . . . . . 8
⊢ ;30 ∈ ℂ | 
| 97 | 96 | addridi 11449 | . . . . . . 7
⊢ (;30 + 0) = ;30 | 
| 98 | 95, 97 | eqtri 2764 | . . . . . 6
⊢ ((2
· ;15) + 0) = ;30 | 
| 99 |  | 3cn 12348 | . . . . . . . 8
⊢ 3 ∈
ℂ | 
| 100 |  | 3t2e6 12433 | . . . . . . . 8
⊢ (3
· 2) = 6 | 
| 101 | 99, 57, 100 | mulcomli 11271 | . . . . . . 7
⊢ (2
· 3) = 6 | 
| 102 | 2 | dec0h 12757 | . . . . . . 7
⊢ 6 = ;06 | 
| 103 | 101, 102 | eqtri 2764 | . . . . . 6
⊢ (2
· 3) = ;06 | 
| 104 | 3, 46, 29, 87, 2, 39, 98, 103 | decmul2c 12801 | . . . . 5
⊢ (2
· ;;153) = ;;306 | 
| 105 | 67 | mullidi 11267 | . . . . . . . 8
⊢ (1
· 𝑁) = 𝑁 | 
| 106 | 105, 17 | eqtri 2764 | . . . . . . 7
⊢ (1
· 𝑁) = ;;;1259 | 
| 107 |  | eqid 2736 | . . . . . . 7
⊢ ;;;1241 =
;;;1241 | 
| 108 | 3, 30 | deccl 12750 | . . . . . . . 8
⊢ ;24 ∈
ℕ0 | 
| 109 |  | eqid 2736 | . . . . . . . . 9
⊢ ;24 = ;24 | 
| 110 | 3, 30, 55, 109 | decsuc 12766 | . . . . . . . 8
⊢ (;24 + 1) = ;25 | 
| 111 |  | eqid 2736 | . . . . . . . . 9
⊢ ;;125 = ;;125 | 
| 112 |  | eqid 2736 | . . . . . . . . 9
⊢ ;;124 = ;;124 | 
| 113 |  | eqid 2736 | . . . . . . . . . 10
⊢ ;12 = ;12 | 
| 114 |  | 1p1e2 12392 | . . . . . . . . . 10
⊢ (1 + 1) =
2 | 
| 115 |  | 2p2e4 12402 | . . . . . . . . . 10
⊢ (2 + 2) =
4 | 
| 116 | 9, 3, 9, 3, 113, 113, 114, 115 | decadd 12789 | . . . . . . . . 9
⊢ (;12 + ;12) = ;24 | 
| 117 |  | 5p4e9 12425 | . . . . . . . . 9
⊢ (5 + 4) =
9 | 
| 118 | 10, 11, 10, 30, 111, 112, 116, 117 | decadd 12789 | . . . . . . . 8
⊢ (;;125 + ;;124) =
;;249 | 
| 119 | 108, 110,
118 | decsucc 12776 | . . . . . . 7
⊢ ((;;125 + ;;124) +
1) = ;;250 | 
| 120 |  | 9p1e10 12737 | . . . . . . 7
⊢ (9 + 1) =
;10 | 
| 121 | 12, 5, 44, 9, 106, 107, 119, 120 | decaddc2 12791 | . . . . . 6
⊢ ((1
· 𝑁) + ;;;1241)
= ;;;2500 | 
| 122 |  | eqid 2736 | . . . . . . 7
⊢ ;50 = ;50 | 
| 123 | 92 | mul02i 11451 | . . . . . . . . . 10
⊢ (0
· 5) = 0 | 
| 124 | 11, 11, 39, 122, 70, 123 | decmul1 12799 | . . . . . . . . 9
⊢ (;50 · 5) = ;;250 | 
| 125 | 124 | oveq1i 7442 | . . . . . . . 8
⊢ ((;50 · 5) + 0) = (;;250 + 0) | 
| 126 | 51, 39 | deccl 12750 | . . . . . . . . . 10
⊢ ;;250 ∈ ℕ0 | 
| 127 | 126 | nn0cni 12540 | . . . . . . . . 9
⊢ ;;250 ∈ ℂ | 
| 128 | 127 | addridi 11449 | . . . . . . . 8
⊢ (;;250 + 0) = ;;250 | 
| 129 | 125, 128 | eqtri 2764 | . . . . . . 7
⊢ ((;50 · 5) + 0) = ;;250 | 
| 130 | 76 | mul01i 11452 | . . . . . . . 8
⊢ (;50 · 0) = 0 | 
| 131 | 39 | dec0h 12757 | . . . . . . . 8
⊢ 0 = ;00 | 
| 132 | 130, 131 | eqtri 2764 | . . . . . . 7
⊢ (;50 · 0) = ;00 | 
| 133 | 49, 11, 39, 122, 39, 39, 129, 132 | decmul2c 12801 | . . . . . 6
⊢ (;50 · ;50) = ;;;2500 | 
| 134 | 121, 133 | eqtr4i 2767 | . . . . 5
⊢ ((1
· 𝑁) + ;;;1241)
= (;50 · ;50) | 
| 135 | 26, 1, 47, 48, 49, 45, 86, 104, 134 | mod2xi 17108 | . . . 4
⊢
((2↑;;306) mod 𝑁) = (;;;1241 mod 𝑁) | 
| 136 |  | eqid 2736 | . . . . 5
⊢ ;;306 = ;;306 | 
| 137 |  | eqid 2736 | . . . . . 6
⊢ ;30 = ;30 | 
| 138 | 9 | dec0h 12757 | . . . . . 6
⊢ 1 = ;01 | 
| 139 |  | 00id 11437 | . . . . . . . 8
⊢ (0 + 0) =
0 | 
| 140 | 101, 139 | oveq12i 7444 | . . . . . . 7
⊢ ((2
· 3) + (0 + 0)) = (6 + 0) | 
| 141 | 61 | addridi 11449 | . . . . . . 7
⊢ (6 + 0) =
6 | 
| 142 | 140, 141 | eqtri 2764 | . . . . . 6
⊢ ((2
· 3) + (0 + 0)) = 6 | 
| 143 | 57 | mul01i 11452 | . . . . . . . 8
⊢ (2
· 0) = 0 | 
| 144 | 143 | oveq1i 7442 | . . . . . . 7
⊢ ((2
· 0) + 1) = (0 + 1) | 
| 145 |  | 0p1e1 12389 | . . . . . . 7
⊢ (0 + 1) =
1 | 
| 146 | 144, 145,
138 | 3eqtri 2768 | . . . . . 6
⊢ ((2
· 0) + 1) = ;01 | 
| 147 | 29, 39, 39, 9, 137, 138, 3, 9, 39, 142, 146 | decma2c 12788 | . . . . 5
⊢ ((2
· ;30) + 1) = ;61 | 
| 148 | 3, 40, 2, 136, 3, 9, 147, 63 | decmul2c 12801 | . . . 4
⊢ (2
· ;;306) = ;;612 | 
| 149 |  | eqid 2736 | . . . . . 6
⊢ ;18 = ;18 | 
| 150 | 10, 30, 55, 112 | decsuc 12766 | . . . . . 6
⊢ (;;124 + 1) = ;;125 | 
| 151 |  | 8cn 12364 | . . . . . . 7
⊢ 8 ∈
ℂ | 
| 152 | 151, 16, 18 | addcomli 11454 | . . . . . 6
⊢ (1 + 8) =
9 | 
| 153 | 44, 9, 9, 13, 107, 149, 150, 152 | decadd 12789 | . . . . 5
⊢ (;;;1241 +
;18) = ;;;1259 | 
| 154 | 153, 17 | eqtr4i 2767 | . . . 4
⊢ (;;;1241 +
;18) = 𝑁 | 
| 155 | 34 | nn0cni 12540 | . . . . . 6
⊢ ;;324 ∈ ℂ | 
| 156 | 155 | addlidi 11450 | . . . . 5
⊢ (0 +
;;324) = ;;324 | 
| 157 | 68 | oveq1i 7442 | . . . . 5
⊢ ((0
· 𝑁) + ;;324) = (0 + ;;324) | 
| 158 | 9, 13 | deccl 12750 | . . . . . 6
⊢ ;18 ∈
ℕ0 | 
| 159 | 9, 30 | deccl 12750 | . . . . . 6
⊢ ;14 ∈
ℕ0 | 
| 160 |  | eqid 2736 | . . . . . . 7
⊢ ;14 = ;14 | 
| 161 | 16 | mulridi 11266 | . . . . . . . . 9
⊢ (1
· 1) = 1 | 
| 162 | 161, 114 | oveq12i 7444 | . . . . . . . 8
⊢ ((1
· 1) + (1 + 1)) = (1 + 2) | 
| 163 |  | 1p2e3 12410 | . . . . . . . 8
⊢ (1 + 2) =
3 | 
| 164 | 162, 163 | eqtri 2764 | . . . . . . 7
⊢ ((1
· 1) + (1 + 1)) = 3 | 
| 165 | 151 | mulridi 11266 | . . . . . . . . 9
⊢ (8
· 1) = 8 | 
| 166 | 165 | oveq1i 7442 | . . . . . . . 8
⊢ ((8
· 1) + 4) = (8 + 4) | 
| 167 |  | 8p4e12 12817 | . . . . . . . 8
⊢ (8 + 4) =
;12 | 
| 168 | 166, 167 | eqtri 2764 | . . . . . . 7
⊢ ((8
· 1) + 4) = ;12 | 
| 169 | 9, 13, 9, 30, 149, 160, 9, 3, 9, 164, 168 | decmac 12787 | . . . . . 6
⊢ ((;18 · 1) + ;14) = ;32 | 
| 170 | 151 | mullidi 11267 | . . . . . . . . 9
⊢ (1
· 8) = 8 | 
| 171 | 170 | oveq1i 7442 | . . . . . . . 8
⊢ ((1
· 8) + 6) = (8 + 6) | 
| 172 |  | 8p6e14 12819 | . . . . . . . 8
⊢ (8 + 6) =
;14 | 
| 173 | 171, 172 | eqtri 2764 | . . . . . . 7
⊢ ((1
· 8) + 6) = ;14 | 
| 174 |  | 8t8e64 12856 | . . . . . . 7
⊢ (8
· 8) = ;64 | 
| 175 | 13, 9, 13, 149, 30, 2, 173, 174 | decmul1c 12800 | . . . . . 6
⊢ (;18 · 8) = ;;144 | 
| 176 | 158, 9, 13, 149, 30, 159, 169, 175 | decmul2c 12801 | . . . . 5
⊢ (;18 · ;18) = ;;324 | 
| 177 | 156, 157,
176 | 3eqtr4i 2774 | . . . 4
⊢ ((0
· 𝑁) + ;;324) = (;18 · ;18) | 
| 178 | 1, 41, 7, 43, 34, 45, 135, 148, 154, 177 | mod2xnegi 17110 | . . 3
⊢
((2↑;;612) mod 𝑁) = (;;324
mod 𝑁) | 
| 179 | 17 | 1259lem1 17169 | . . 3
⊢
((2↑;17) mod 𝑁) = (;;136
mod 𝑁) | 
| 180 |  | eqid 2736 | . . . 4
⊢ ;;612 = ;;612 | 
| 181 |  | eqid 2736 | . . . 4
⊢ ;17 = ;17 | 
| 182 |  | eqid 2736 | . . . . 5
⊢ ;61 = ;61 | 
| 183 | 2, 9, 114, 182 | decsuc 12766 | . . . 4
⊢ (;61 + 1) = ;62 | 
| 184 |  | 7p2e9 12428 | . . . . 5
⊢ (7 + 2) =
9 | 
| 185 | 56, 57, 184 | addcomli 11454 | . . . 4
⊢ (2 + 7) =
9 | 
| 186 | 27, 3, 9, 35, 180, 181, 183, 185 | decadd 12789 | . . 3
⊢ (;;612 + ;17) = ;;629 | 
| 187 | 29, 9 | deccl 12750 | . . . . 5
⊢ ;31 ∈
ℕ0 | 
| 188 |  | eqid 2736 | . . . . . . 7
⊢ ;31 = ;31 | 
| 189 |  | 3p2e5 12418 | . . . . . . . . 9
⊢ (3 + 2) =
5 | 
| 190 | 99, 57, 189 | addcomli 11454 | . . . . . . . 8
⊢ (2 + 3) =
5 | 
| 191 | 9, 3, 29, 113, 190 | decaddi 12795 | . . . . . . 7
⊢ (;12 + 3) = ;15 | 
| 192 |  | 5p1e6 12414 | . . . . . . 7
⊢ (5 + 1) =
6 | 
| 193 | 10, 11, 29, 9, 111, 188, 191, 192 | decadd 12789 | . . . . . 6
⊢ (;;125 + ;31) = ;;156 | 
| 194 | 114 | oveq1i 7442 | . . . . . . . . 9
⊢ ((1 + 1)
+ 1) = (2 + 1) | 
| 195 | 194, 73 | eqtri 2764 | . . . . . . . 8
⊢ ((1 + 1)
+ 1) = 3 | 
| 196 |  | 7p5e12 12812 | . . . . . . . . 9
⊢ (7 + 5) =
;12 | 
| 197 | 56, 92, 196 | addcomli 11454 | . . . . . . . 8
⊢ (5 + 7) =
;12 | 
| 198 | 9, 11, 9, 35, 88, 181, 195, 3, 197 | decaddc 12790 | . . . . . . 7
⊢ (;15 + ;17) = ;32 | 
| 199 |  | eqid 2736 | . . . . . . . 8
⊢ ;34 = ;34 | 
| 200 |  | 7p3e10 12810 | . . . . . . . . 9
⊢ (7 + 3) =
;10 | 
| 201 | 56, 99, 200 | addcomli 11454 | . . . . . . . 8
⊢ (3 + 7) =
;10 | 
| 202 | 99 | mulridi 11266 | . . . . . . . . . 10
⊢ (3
· 1) = 3 | 
| 203 | 16 | addridi 11449 | . . . . . . . . . 10
⊢ (1 + 0) =
1 | 
| 204 | 202, 203 | oveq12i 7444 | . . . . . . . . 9
⊢ ((3
· 1) + (1 + 0)) = (3 + 1) | 
| 205 |  | 3p1e4 12412 | . . . . . . . . 9
⊢ (3 + 1) =
4 | 
| 206 | 204, 205 | eqtri 2764 | . . . . . . . 8
⊢ ((3
· 1) + (1 + 0)) = 4 | 
| 207 |  | 4cn 12352 | . . . . . . . . . . 11
⊢ 4 ∈
ℂ | 
| 208 | 207 | mulridi 11266 | . . . . . . . . . 10
⊢ (4
· 1) = 4 | 
| 209 | 208 | oveq1i 7442 | . . . . . . . . 9
⊢ ((4
· 1) + 0) = (4 + 0) | 
| 210 | 207 | addridi 11449 | . . . . . . . . 9
⊢ (4 + 0) =
4 | 
| 211 | 30 | dec0h 12757 | . . . . . . . . 9
⊢ 4 = ;04 | 
| 212 | 209, 210,
211 | 3eqtri 2768 | . . . . . . . 8
⊢ ((4
· 1) + 0) = ;04 | 
| 213 | 29, 30, 9, 39, 199, 201, 9, 30, 39, 206, 212 | decmac 12787 | . . . . . . 7
⊢ ((;34 · 1) + (3 + 7)) = ;44 | 
| 214 | 3 | dec0h 12757 | . . . . . . . 8
⊢ 2 = ;02 | 
| 215 | 100, 145 | oveq12i 7444 | . . . . . . . . 9
⊢ ((3
· 2) + (0 + 1)) = (6 + 1) | 
| 216 |  | 6p1e7 12415 | . . . . . . . . 9
⊢ (6 + 1) =
7 | 
| 217 | 215, 216 | eqtri 2764 | . . . . . . . 8
⊢ ((3
· 2) + (0 + 1)) = 7 | 
| 218 |  | 4t2e8 12435 | . . . . . . . . . 10
⊢ (4
· 2) = 8 | 
| 219 | 218 | oveq1i 7442 | . . . . . . . . 9
⊢ ((4
· 2) + 2) = (8 + 2) | 
| 220 |  | 8p2e10 12815 | . . . . . . . . 9
⊢ (8 + 2) =
;10 | 
| 221 | 219, 220 | eqtri 2764 | . . . . . . . 8
⊢ ((4
· 2) + 2) = ;10 | 
| 222 | 29, 30, 39, 3, 199, 214, 3, 39, 9, 217, 221 | decmac 12787 | . . . . . . 7
⊢ ((;34 · 2) + 2) = ;70 | 
| 223 | 9, 3, 29, 3, 113, 198, 31, 39, 35, 213, 222 | decma2c 12788 | . . . . . 6
⊢ ((;34 · ;12) + (;15 + ;17)) = ;;440 | 
| 224 |  | 5t3e15 12836 | . . . . . . . . 9
⊢ (5
· 3) = ;15 | 
| 225 | 92, 99, 224 | mulcomli 11271 | . . . . . . . 8
⊢ (3
· 5) = ;15 | 
| 226 |  | 5p2e7 12423 | . . . . . . . 8
⊢ (5 + 2) =
7 | 
| 227 | 9, 11, 3, 225, 226 | decaddi 12795 | . . . . . . 7
⊢ ((3
· 5) + 2) = ;17 | 
| 228 |  | 5t4e20 12837 | . . . . . . . . 9
⊢ (5
· 4) = ;20 | 
| 229 | 92, 207, 228 | mulcomli 11271 | . . . . . . . 8
⊢ (4
· 5) = ;20 | 
| 230 | 61 | addlidi 11450 | . . . . . . . 8
⊢ (0 + 6) =
6 | 
| 231 | 3, 39, 2, 229, 230 | decaddi 12795 | . . . . . . 7
⊢ ((4
· 5) + 6) = ;26 | 
| 232 | 29, 30, 2, 199, 11, 2, 3, 227, 231 | decrmac 12793 | . . . . . 6
⊢ ((;34 · 5) + 6) = ;;176 | 
| 233 | 10, 11, 46, 2, 111, 193, 31, 2, 36, 223, 232 | decma2c 12788 | . . . . 5
⊢ ((;34 · ;;125) +
(;;125 + ;31)) = ;;;4406 | 
| 234 |  | 9cn 12367 | . . . . . . . 8
⊢ 9 ∈
ℂ | 
| 235 |  | 9t3e27 12858 | . . . . . . . 8
⊢ (9
· 3) = ;27 | 
| 236 | 234, 99, 235 | mulcomli 11271 | . . . . . . 7
⊢ (3
· 9) = ;27 | 
| 237 |  | 7p4e11 12811 | . . . . . . 7
⊢ (7 + 4) =
;11 | 
| 238 | 3, 35, 30, 236, 73, 9, 237 | decaddci 12796 | . . . . . 6
⊢ ((3
· 9) + 4) = ;31 | 
| 239 |  | 9t4e36 12859 | . . . . . . . 8
⊢ (9
· 4) = ;36 | 
| 240 | 234, 207,
239 | mulcomli 11271 | . . . . . . 7
⊢ (4
· 9) = ;36 | 
| 241 | 151, 61, 172 | addcomli 11454 | . . . . . . 7
⊢ (6 + 8) =
;14 | 
| 242 | 29, 2, 13, 240, 205, 30, 241 | decaddci 12796 | . . . . . 6
⊢ ((4
· 9) + 8) = ;44 | 
| 243 | 29, 30, 13, 199, 5, 30, 30, 238, 242 | decrmac 12793 | . . . . 5
⊢ ((;34 · 9) + 8) = ;;314 | 
| 244 | 12, 5, 12, 13, 17, 22, 31, 30, 187, 233, 243 | decma2c 12788 | . . . 4
⊢ ((;34 · 𝑁) + (𝑁 − 1)) = ;;;;44064 | 
| 245 |  | eqid 2736 | . . . . 5
⊢ ;;136 = ;;136 | 
| 246 | 9, 5 | deccl 12750 | . . . . . 6
⊢ ;19 ∈
ℕ0 | 
| 247 | 246, 30 | deccl 12750 | . . . . 5
⊢ ;;194 ∈ ℕ0 | 
| 248 |  | eqid 2736 | . . . . . 6
⊢ ;13 = ;13 | 
| 249 |  | eqid 2736 | . . . . . 6
⊢ ;;194 = ;;194 | 
| 250 | 5, 35 | deccl 12750 | . . . . . 6
⊢ ;97 ∈
ℕ0 | 
| 251 | 9, 9 | deccl 12750 | . . . . . . 7
⊢ ;11 ∈
ℕ0 | 
| 252 |  | eqid 2736 | . . . . . . 7
⊢ ;;324 = ;;324 | 
| 253 |  | eqid 2736 | . . . . . . . 8
⊢ ;19 = ;19 | 
| 254 |  | eqid 2736 | . . . . . . . 8
⊢ ;97 = ;97 | 
| 255 | 234, 16, 120 | addcomli 11454 | . . . . . . . . 9
⊢ (1 + 9) =
;10 | 
| 256 | 9, 39, 145, 255 | decsuc 12766 | . . . . . . . 8
⊢ ((1 + 9)
+ 1) = ;11 | 
| 257 |  | 9p7e16 12827 | . . . . . . . 8
⊢ (9 + 7) =
;16 | 
| 258 | 9, 5, 5, 35, 253, 254, 256, 2, 257 | decaddc 12790 | . . . . . . 7
⊢ (;19 + ;97) = ;;116 | 
| 259 |  | eqid 2736 | . . . . . . . 8
⊢ ;32 = ;32 | 
| 260 |  | eqid 2736 | . . . . . . . . 9
⊢ ;11 = ;11 | 
| 261 | 9, 9, 114, 260 | decsuc 12766 | . . . . . . . 8
⊢ (;11 + 1) = ;12 | 
| 262 | 89 | oveq1i 7442 | . . . . . . . . 9
⊢ ((2
· 1) + 2) = (2 + 2) | 
| 263 | 262, 115,
211 | 3eqtri 2768 | . . . . . . . 8
⊢ ((2
· 1) + 2) = ;04 | 
| 264 | 29, 3, 9, 3, 259, 261, 9, 30, 39, 206, 263 | decmac 12787 | . . . . . . 7
⊢ ((;32 · 1) + (;11 + 1)) = ;44 | 
| 265 | 208 | oveq1i 7442 | . . . . . . . 8
⊢ ((4
· 1) + 6) = (4 + 6) | 
| 266 |  | 6p4e10 12807 | . . . . . . . . 9
⊢ (6 + 4) =
;10 | 
| 267 | 61, 207, 266 | addcomli 11454 | . . . . . . . 8
⊢ (4 + 6) =
;10 | 
| 268 | 265, 267 | eqtri 2764 | . . . . . . 7
⊢ ((4
· 1) + 6) = ;10 | 
| 269 | 33, 30, 251, 2, 252, 258, 9, 39, 9, 264, 268 | decmac 12787 | . . . . . 6
⊢ ((;;324 · 1) + (;19 + ;97)) = ;;440 | 
| 270 | 145, 138 | eqtri 2764 | . . . . . . . 8
⊢ (0 + 1) =
;01 | 
| 271 |  | 3t3e9 12434 | . . . . . . . . . 10
⊢ (3
· 3) = 9 | 
| 272 | 271, 139 | oveq12i 7444 | . . . . . . . . 9
⊢ ((3
· 3) + (0 + 0)) = (9 + 0) | 
| 273 | 234 | addridi 11449 | . . . . . . . . 9
⊢ (9 + 0) =
9 | 
| 274 | 272, 273 | eqtri 2764 | . . . . . . . 8
⊢ ((3
· 3) + (0 + 0)) = 9 | 
| 275 | 101 | oveq1i 7442 | . . . . . . . . 9
⊢ ((2
· 3) + 1) = (6 + 1) | 
| 276 | 35 | dec0h 12757 | . . . . . . . . 9
⊢ 7 = ;07 | 
| 277 | 275, 216,
276 | 3eqtri 2768 | . . . . . . . 8
⊢ ((2
· 3) + 1) = ;07 | 
| 278 | 29, 3, 39, 9, 259, 270, 29, 35, 39, 274, 277 | decmac 12787 | . . . . . . 7
⊢ ((;32 · 3) + (0 + 1)) = ;97 | 
| 279 |  | 4t3e12 12833 | . . . . . . . 8
⊢ (4
· 3) = ;12 | 
| 280 |  | 4p2e6 12420 | . . . . . . . . 9
⊢ (4 + 2) =
6 | 
| 281 | 207, 57, 280 | addcomli 11454 | . . . . . . . 8
⊢ (2 + 4) =
6 | 
| 282 | 9, 3, 30, 279, 281 | decaddi 12795 | . . . . . . 7
⊢ ((4
· 3) + 4) = ;16 | 
| 283 | 33, 30, 39, 30, 252, 211, 29, 2, 9, 278, 282 | decmac 12787 | . . . . . 6
⊢ ((;;324 · 3) + 4) = ;;976 | 
| 284 | 9, 29, 246, 30, 248, 249, 34, 2, 250, 269, 283 | decma2c 12788 | . . . . 5
⊢ ((;;324 · ;13) + ;;194) =
;;;4406 | 
| 285 |  | 6t3e18 12840 | . . . . . . . . 9
⊢ (6
· 3) = ;18 | 
| 286 | 61, 99, 285 | mulcomli 11271 | . . . . . . . 8
⊢ (3
· 6) = ;18 | 
| 287 | 9, 13, 18, 286 | decsuc 12766 | . . . . . . 7
⊢ ((3
· 6) + 1) = ;19 | 
| 288 | 9, 3, 3, 63, 115 | decaddi 12795 | . . . . . . 7
⊢ ((2
· 6) + 2) = ;14 | 
| 289 | 29, 3, 3, 259, 2, 30, 9, 287, 288 | decrmac 12793 | . . . . . 6
⊢ ((;32 · 6) + 2) = ;;194 | 
| 290 |  | 6t4e24 12841 | . . . . . . 7
⊢ (6
· 4) = ;24 | 
| 291 | 61, 207, 290 | mulcomli 11271 | . . . . . 6
⊢ (4
· 6) = ;24 | 
| 292 | 2, 33, 30, 252, 30, 3, 289, 291 | decmul1c 12800 | . . . . 5
⊢ (;;324 · 6) = ;;;1944 | 
| 293 | 34, 37, 2, 245, 30, 247, 284, 292 | decmul2c 12801 | . . . 4
⊢ (;;324 · ;;136) =
;;;;44064 | 
| 294 | 244, 293 | eqtr4i 2767 | . . 3
⊢ ((;34 · 𝑁) + (𝑁 − 1)) = (;;324
· ;;136) | 
| 295 | 26, 1, 28, 32, 34, 23, 36, 38, 178, 179, 186, 294 | modxai 17107 | . 2
⊢
((2↑;;629) mod 𝑁) = ((𝑁 − 1) mod 𝑁) | 
| 296 |  | eqid 2736 | . . . 4
⊢ ;;629 = ;;629 | 
| 297 |  | eqid 2736 | . . . . 5
⊢ ;62 = ;62 | 
| 298 | 139 | oveq2i 7443 | . . . . . 6
⊢ ((2
· 6) + (0 + 0)) = ((2 · 6) + 0) | 
| 299 | 63 | oveq1i 7442 | . . . . . 6
⊢ ((2
· 6) + 0) = (;12 +
0) | 
| 300 | 10 | nn0cni 12540 | . . . . . . 7
⊢ ;12 ∈ ℂ | 
| 301 | 300 | addridi 11449 | . . . . . 6
⊢ (;12 + 0) = ;12 | 
| 302 | 298, 299,
301 | 3eqtri 2768 | . . . . 5
⊢ ((2
· 6) + (0 + 0)) = ;12 | 
| 303 | 11 | dec0h 12757 | . . . . . 6
⊢ 5 = ;05 | 
| 304 | 81, 55, 303 | 3eqtri 2768 | . . . . 5
⊢ ((2
· 2) + 1) = ;05 | 
| 305 | 2, 3, 39, 9, 297, 138, 3, 11, 39, 302, 304 | decma2c 12788 | . . . 4
⊢ ((2
· ;62) + 1) = ;;125 | 
| 306 |  | 9t2e18 12857 | . . . . 5
⊢ (9
· 2) = ;18 | 
| 307 | 234, 57, 306 | mulcomli 11271 | . . . 4
⊢ (2
· 9) = ;18 | 
| 308 | 3, 4, 5, 296, 13, 9, 305, 307 | decmul2c 12801 | . . 3
⊢ (2
· ;;629) = ;;;1258 | 
| 309 | 308, 22 | eqtr4i 2767 | . 2
⊢ (2
· ;;629) = (𝑁 − 1) | 
| 310 |  | npcan 11518 | . . 3
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) | 
| 311 | 67, 16, 310 | mp2an 692 | . 2
⊢ ((𝑁 − 1) + 1) = 𝑁 | 
| 312 | 68 | oveq1i 7442 | . . 3
⊢ ((0
· 𝑁) + 1) = (0 +
1) | 
| 313 | 145, 312,
161 | 3eqtr4i 2774 | . 2
⊢ ((0
· 𝑁) + 1) = (1
· 1) | 
| 314 | 1, 6, 7, 8, 9, 23,
295, 309, 311, 313 | mod2xnegi 17110 | 1
⊢
((2↑(𝑁 −
1)) mod 𝑁) = (1 mod 𝑁) |