# Metamath Proof Explorer

## Theorem 4001lem1

Description: Lemma for 4001prm . Calculate a power mod. In decimal, we calculate 2 ^ 1 2 = 4 0 9 6 = N + 9 5 , 2 ^ 2 4 = ( 2 ^ 1 2 ) ^ 2 == 9 5 ^ 2 = 2 N + 1 0 2 3 , 2 ^ 2 5 = 2 ^ 2 4 x. 2 == 1 0 2 3 x. 2 = 2 0 4 6 , 2 ^ 5 0 = ( 2 ^ 2 5 ) ^ 2 == 2 0 4 6 ^ 2 = 1 0 4 6 N + 1 0 7 0 , 2 ^ 1 0 0 = ( 2 ^ 5 0 ) ^ 2 == 1 0 7 0 ^ 2 = 2 8 6 N + 6 1 4 and 2 ^ 2 0 0 = ( 2 ^ 1 0 0 ) ^ 2 == 6 1 4 ^ 2 = 9 4 N + 9 0 2 == 9 0 2 . (Contributed by Mario Carneiro, 3-Mar-2014) (Revised by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

Ref Expression
Hypothesis 4001prm.1 ${⊢}{N}=4001$
Assertion 4001lem1 ${⊢}{2}^{200}\mathrm{mod}{N}=902\mathrm{mod}{N}$

### Proof

Step Hyp Ref Expression
1 4001prm.1 ${⊢}{N}=4001$
2 4nn0 ${⊢}4\in {ℕ}_{0}$
3 0nn0 ${⊢}0\in {ℕ}_{0}$
4 2 3 deccl ${⊢}40\in {ℕ}_{0}$
5 4 3 deccl ${⊢}400\in {ℕ}_{0}$
6 1nn ${⊢}1\in ℕ$
7 5 6 decnncl ${⊢}4001\in ℕ$
8 1 7 eqeltri ${⊢}{N}\in ℕ$
9 2nn ${⊢}2\in ℕ$
10 10nn0 ${⊢}10\in {ℕ}_{0}$
11 10 3 deccl ${⊢}100\in {ℕ}_{0}$
12 9nn0 ${⊢}9\in {ℕ}_{0}$
13 12 2 deccl ${⊢}94\in {ℕ}_{0}$
14 13 nn0zi ${⊢}94\in ℤ$
15 6nn0 ${⊢}6\in {ℕ}_{0}$
16 1nn0 ${⊢}1\in {ℕ}_{0}$
17 15 16 deccl ${⊢}61\in {ℕ}_{0}$
18 17 2 deccl ${⊢}614\in {ℕ}_{0}$
19 12 3 deccl ${⊢}90\in {ℕ}_{0}$
20 2nn0 ${⊢}2\in {ℕ}_{0}$
21 19 20 deccl ${⊢}902\in {ℕ}_{0}$
22 5nn0 ${⊢}5\in {ℕ}_{0}$
23 22 3 deccl ${⊢}50\in {ℕ}_{0}$
24 8nn0 ${⊢}8\in {ℕ}_{0}$
25 20 24 deccl ${⊢}28\in {ℕ}_{0}$
26 25 15 deccl ${⊢}286\in {ℕ}_{0}$
27 26 nn0zi ${⊢}286\in ℤ$
28 7nn0 ${⊢}7\in {ℕ}_{0}$
29 10 28 deccl ${⊢}107\in {ℕ}_{0}$
30 29 3 deccl ${⊢}1070\in {ℕ}_{0}$
31 20 22 deccl ${⊢}25\in {ℕ}_{0}$
32 10 2 deccl ${⊢}104\in {ℕ}_{0}$
33 32 15 deccl ${⊢}1046\in {ℕ}_{0}$
34 33 nn0zi ${⊢}1046\in ℤ$
35 20 3 deccl ${⊢}20\in {ℕ}_{0}$
36 35 2 deccl ${⊢}204\in {ℕ}_{0}$
37 36 15 deccl ${⊢}2046\in {ℕ}_{0}$
38 20 2 deccl ${⊢}24\in {ℕ}_{0}$
39 0z ${⊢}0\in ℤ$
40 10 20 deccl ${⊢}102\in {ℕ}_{0}$
41 3nn0 ${⊢}3\in {ℕ}_{0}$
42 40 41 deccl ${⊢}1023\in {ℕ}_{0}$
43 16 20 deccl ${⊢}12\in {ℕ}_{0}$
44 2z ${⊢}2\in ℤ$
45 12 22 deccl ${⊢}95\in {ℕ}_{0}$
46 1z ${⊢}1\in ℤ$
47 15 2 deccl ${⊢}64\in {ℕ}_{0}$
48 2exp6 ${⊢}{2}^{6}=64$
49 48 oveq1i ${⊢}{2}^{6}\mathrm{mod}{N}=64\mathrm{mod}{N}$
50 6cn ${⊢}6\in ℂ$
51 2cn ${⊢}2\in ℂ$
52 6t2e12 ${⊢}6\cdot 2=12$
53 50 51 52 mulcomli ${⊢}2\cdot 6=12$
54 eqid ${⊢}95=95$
55 eqid ${⊢}400=400$
56 9cn ${⊢}9\in ℂ$
57 56 addid1i ${⊢}9+0=9$
58 12 dec0h ${⊢}9=09$
59 57 58 eqtri ${⊢}9+0=09$
60 eqid ${⊢}40=40$
61 00id ${⊢}0+0=0$
62 3 dec0h ${⊢}0=00$
63 61 62 eqtri ${⊢}0+0=00$
64 4cn ${⊢}4\in ℂ$
65 64 mulid2i ${⊢}1\cdot 4=4$
66 65 61 oveq12i ${⊢}1\cdot 4+0+0=4+0$
67 64 addid1i ${⊢}4+0=4$
68 66 67 eqtri ${⊢}1\cdot 4+0+0=4$
69 ax-1cn ${⊢}1\in ℂ$
70 69 mul01i ${⊢}1\cdot 0=0$
71 70 oveq1i ${⊢}1\cdot 0+0=0+0$
72 71 61 62 3eqtri ${⊢}1\cdot 0+0=00$
73 2 3 3 3 60 63 16 3 3 68 72 decma2c ${⊢}1\cdot 40+0+0=40$
74 70 oveq1i ${⊢}1\cdot 0+9=0+9$
75 56 addid2i ${⊢}0+9=9$
76 74 75 58 3eqtri ${⊢}1\cdot 0+9=09$
77 4 3 3 12 55 59 16 12 3 73 76 decma2c ${⊢}1\cdot 400+9+0=409$
78 69 mulid1i ${⊢}1\cdot 1=1$
79 78 oveq1i ${⊢}1\cdot 1+5=1+5$
80 5cn ${⊢}5\in ℂ$
81 5p1e6 ${⊢}5+1=6$
82 80 69 81 addcomli ${⊢}1+5=6$
83 15 dec0h ${⊢}6=06$
84 79 82 83 3eqtri ${⊢}1\cdot 1+5=06$
85 5 16 12 22 1 54 16 15 3 77 84 decma2c ${⊢}1\cdot {N}+95=4096$
86 eqid ${⊢}64=64$
87 eqid ${⊢}25=25$
88 2p2e4 ${⊢}2+2=4$
89 88 oveq2i ${⊢}6\cdot 6+2+2=6\cdot 6+4$
90 6t6e36 ${⊢}6\cdot 6=36$
91 3p1e4 ${⊢}3+1=4$
92 6p4e10 ${⊢}6+4=10$
93 41 15 2 90 91 92 decaddci2 ${⊢}6\cdot 6+4=40$
94 89 93 eqtri ${⊢}6\cdot 6+2+2=40$
95 6t4e24 ${⊢}6\cdot 4=24$
96 50 64 95 mulcomli ${⊢}4\cdot 6=24$
97 5p4e9 ${⊢}5+4=9$
98 80 64 97 addcomli ${⊢}4+5=9$
99 20 2 22 96 98 decaddi ${⊢}4\cdot 6+5=29$
100 15 2 20 22 86 87 15 12 20 94 99 decmac ${⊢}64\cdot 6+25=409$
101 4p1e5 ${⊢}4+1=5$
102 20 2 101 95 decsuc ${⊢}6\cdot 4+1=25$
103 4t4e16 ${⊢}4\cdot 4=16$
104 2 15 2 86 15 16 102 103 decmul1c ${⊢}64\cdot 4=256$
105 47 15 2 86 15 31 100 104 decmul2c ${⊢}64\cdot 64=4096$
106 85 105 eqtr4i ${⊢}1\cdot {N}+95=64\cdot 64$
107 8 9 15 46 47 45 49 53 106 mod2xi ${⊢}{2}^{12}\mathrm{mod}{N}=95\mathrm{mod}{N}$
108 eqid ${⊢}12=12$
109 51 mulid1i ${⊢}2\cdot 1=2$
110 109 oveq1i ${⊢}2\cdot 1+0=2+0$
111 51 addid1i ${⊢}2+0=2$
112 110 111 eqtri ${⊢}2\cdot 1+0=2$
113 2t2e4 ${⊢}2\cdot 2=4$
114 2 dec0h ${⊢}4=04$
115 113 114 eqtri ${⊢}2\cdot 2=04$
116 20 16 20 108 2 3 112 115 decmul2c ${⊢}2\cdot 12=24$
117 eqid ${⊢}1023=1023$
118 40 nn0cni ${⊢}102\in ℂ$
119 118 addid1i ${⊢}102+0=102$
120 dec10p ${⊢}10+0=10$
121 4t2e8 ${⊢}4\cdot 2=8$
122 64 51 121 mulcomli ${⊢}2\cdot 4=8$
123 69 addid1i ${⊢}1+0=1$
124 122 123 oveq12i ${⊢}2\cdot 4+1+0=8+1$
125 8p1e9 ${⊢}8+1=9$
126 124 125 eqtri ${⊢}2\cdot 4+1+0=9$
127 51 mul01i ${⊢}2\cdot 0=0$
128 127 oveq1i ${⊢}2\cdot 0+0=0+0$
129 128 61 62 3eqtri ${⊢}2\cdot 0+0=00$
130 2 3 16 3 60 120 20 3 3 126 129 decma2c ${⊢}2\cdot 40+10+0=90$
131 127 oveq1i ${⊢}2\cdot 0+2=0+2$
132 51 addid2i ${⊢}0+2=2$
133 20 dec0h ${⊢}2=02$
134 131 132 133 3eqtri ${⊢}2\cdot 0+2=02$
135 4 3 10 20 55 119 20 20 3 130 134 decma2c ${⊢}2\cdot 400+102+0=902$
136 109 oveq1i ${⊢}2\cdot 1+3=2+3$
137 3cn ${⊢}3\in ℂ$
138 3p2e5 ${⊢}3+2=5$
139 137 51 138 addcomli ${⊢}2+3=5$
140 22 dec0h ${⊢}5=05$
141 136 139 140 3eqtri ${⊢}2\cdot 1+3=05$
142 5 16 40 41 1 117 20 22 3 135 141 decma2c ${⊢}2\cdot {N}+1023=9025$
143 2 28 deccl ${⊢}47\in {ℕ}_{0}$
144 eqid ${⊢}47=47$
145 98 oveq2i ${⊢}9\cdot 9+4+5=9\cdot 9+9$
146 9t9e81 ${⊢}9\cdot 9=81$
147 9p1e10 ${⊢}9+1=10$
148 56 69 147 addcomli ${⊢}1+9=10$
149 24 16 12 146 125 148 decaddci2 ${⊢}9\cdot 9+9=90$
150 145 149 eqtri ${⊢}9\cdot 9+4+5=90$
151 9t5e45 ${⊢}9\cdot 5=45$
152 56 80 151 mulcomli ${⊢}5\cdot 9=45$
153 7cn ${⊢}7\in ℂ$
154 7p5e12 ${⊢}7+5=12$
155 153 80 154 addcomli ${⊢}5+7=12$
156 2 22 28 152 101 20 155 decaddci ${⊢}5\cdot 9+7=52$
157 12 22 2 28 54 144 12 20 22 150 156 decmac ${⊢}95\cdot 9+47=902$
158 5p2e7 ${⊢}5+2=7$
159 2 22 20 151 158 decaddi ${⊢}9\cdot 5+2=47$
160 5t5e25 ${⊢}5\cdot 5=25$
161 22 12 22 54 22 20 159 160 decmul1c ${⊢}95\cdot 5=475$
162 45 12 22 54 22 143 157 161 decmul2c ${⊢}95\cdot 95=9025$
163 142 162 eqtr4i ${⊢}2\cdot {N}+1023=95\cdot 95$
164 8 9 43 44 45 42 107 116 163 mod2xi ${⊢}{2}^{24}\mathrm{mod}{N}=1023\mathrm{mod}{N}$
165 eqid ${⊢}24=24$
166 20 2 101 165 decsuc ${⊢}24+1=25$
167 37 nn0cni ${⊢}2046\in ℂ$
168 167 addid2i ${⊢}0+2046=2046$
169 8 nncni ${⊢}{N}\in ℂ$
170 169 mul02i ${⊢}0\cdot {N}=0$
171 170 oveq1i ${⊢}0\cdot {N}+2046=0+2046$
172 eqid ${⊢}102=102$
173 20 dec0u ${⊢}10\cdot 2=20$
174 20 10 20 172 173 113 decmul1 ${⊢}102\cdot 2=204$
175 3t2e6 ${⊢}3\cdot 2=6$
176 20 40 41 117 174 175 decmul1 ${⊢}1023\cdot 2=2046$
177 168 171 176 3eqtr4i ${⊢}0\cdot {N}+2046=1023\cdot 2$
178 8 9 38 39 42 37 164 166 177 modxp1i ${⊢}{2}^{25}\mathrm{mod}{N}=2046\mathrm{mod}{N}$
179 113 oveq1i ${⊢}2\cdot 2+1=4+1$
180 179 101 eqtri ${⊢}2\cdot 2+1=5$
181 5t2e10 ${⊢}5\cdot 2=10$
182 80 51 181 mulcomli ${⊢}2\cdot 5=10$
183 20 20 22 87 3 16 180 182 decmul2c ${⊢}2\cdot 25=50$
184 eqid ${⊢}1070=1070$
185 20 16 deccl ${⊢}21\in {ℕ}_{0}$
186 eqid ${⊢}107=107$
187 eqid ${⊢}104=104$
188 0p1e1 ${⊢}0+1=1$
189 10p10e20 ${⊢}10+10=20$
190 20 3 188 189 decsuc ${⊢}10+10+1=21$
191 7p4e11 ${⊢}7+4=11$
192 10 28 10 2 186 187 190 16 191 decaddc ${⊢}107+104=211$
193 185 nn0cni ${⊢}21\in ℂ$
194 193 addid1i ${⊢}21+0=21$
195 111 20 eqeltri ${⊢}2+0\in {ℕ}_{0}$
196 eqid ${⊢}1046=1046$
197 dfdec10 ${⊢}41=10\cdot 4+1$
198 197 eqcomi ${⊢}10\cdot 4+1=41$
199 6p2e8 ${⊢}6+2=8$
200 16 15 20 103 199 decaddi ${⊢}4\cdot 4+2=18$
201 10 2 20 187 2 24 16 198 200 decrmac ${⊢}104\cdot 4+2=418$
202 95 111 oveq12i ${⊢}6\cdot 4+2+0=24+2$
203 4p2e6 ${⊢}4+2=6$
204 20 2 20 165 203 decaddi ${⊢}24+2=26$
205 202 204 eqtri ${⊢}6\cdot 4+2+0=26$
206 32 15 195 196 2 15 20 201 205 decrmac ${⊢}1046\cdot 4+2+0=4186$
207 33 nn0cni ${⊢}1046\in ℂ$
208 207 mul01i ${⊢}1046\cdot 0=0$
209 208 oveq1i ${⊢}1046\cdot 0+1=0+1$
210 16 dec0h ${⊢}1=01$
211 209 188 210 3eqtri ${⊢}1046\cdot 0+1=01$
212 2 3 20 16 60 194 33 16 3 206 211 decma2c ${⊢}1046\cdot 40+21+0=41861$
213 4 3 185 16 55 192 33 16 3 212 211 decma2c ${⊢}1046\cdot 400+107+104=418611$
214 207 mulid1i ${⊢}1046\cdot 1=1046$
215 214 oveq1i ${⊢}1046\cdot 1+0=1046+0$
216 207 addid1i ${⊢}1046+0=1046$
217 215 216 eqtri ${⊢}1046\cdot 1+0=1046$
218 5 16 29 3 1 184 33 15 32 213 217 decma2c ${⊢}1046\cdot {N}+1070=4186116$
219 eqid ${⊢}2046=2046$
220 43 20 deccl ${⊢}122\in {ℕ}_{0}$
221 220 28 deccl ${⊢}1227\in {ℕ}_{0}$
222 eqid ${⊢}204=204$
223 eqid ${⊢}1227=1227$
224 24 16 deccl ${⊢}81\in {ℕ}_{0}$
225 224 12 deccl ${⊢}819\in {ℕ}_{0}$
226 eqid ${⊢}20=20$
227 eqid ${⊢}122=122$
228 eqid ${⊢}819=819$
229 eqid ${⊢}81=81$
230 8cn ${⊢}8\in ℂ$
231 230 69 125 addcomli ${⊢}1+8=9$
232 2p1e3 ${⊢}2+1=3$
233 16 20 24 16 108 229 231 232 decadd ${⊢}12+81=93$
234 12 41 91 233 decsuc ${⊢}12+81+1=94$
235 9p2e11 ${⊢}9+2=11$
236 56 51 235 addcomli ${⊢}2+9=11$
237 43 20 224 12 227 228 234 16 236 decaddc ${⊢}122+819=941$
238 13 nn0cni ${⊢}94\in ℂ$
239 238 addid1i ${⊢}94+0=94$
240 123 16 eqeltri ${⊢}1+0\in {ℕ}_{0}$
241 51 mul02i ${⊢}0\cdot 2=0$
242 241 123 oveq12i ${⊢}0\cdot 2+1+0=0+1$
243 242 188 eqtri ${⊢}0\cdot 2+1+0=1$
244 20 3 240 226 20 113 243 decrmanc ${⊢}20\cdot 2+1+0=41$
245 121 oveq1i ${⊢}4\cdot 2+0=8+0$
246 230 addid1i ${⊢}8+0=8$
247 24 dec0h ${⊢}8=08$
248 245 246 247 3eqtri ${⊢}4\cdot 2+0=08$
249 35 2 16 3 222 147 20 24 3 244 248 decmac ${⊢}204\cdot 2+9+1=418$
250 64 51 203 addcomli ${⊢}2+4=6$
251 16 20 2 52 250 decaddi ${⊢}6\cdot 2+4=16$
252 36 15 12 2 219 239 20 15 16 249 251 decmac ${⊢}2046\cdot 2+94+0=4186$
253 167 mul01i ${⊢}2046\cdot 0=0$
254 253 oveq1i ${⊢}2046\cdot 0+1=0+1$
255 254 188 210 3eqtri ${⊢}2046\cdot 0+1=01$
256 20 3 13 16 226 237 37 16 3 252 255 decma2c ${⊢}2046\cdot 20+122+819=41861$
257 41 dec0h ${⊢}3=03$
258 188 16 eqeltri ${⊢}0+1\in {ℕ}_{0}$
259 64 mul02i ${⊢}0\cdot 4=0$
260 259 188 oveq12i ${⊢}0\cdot 4+0+1=0+1$
261 260 188 eqtri ${⊢}0\cdot 4+0+1=1$
262 20 3 258 226 2 122 261 decrmanc ${⊢}20\cdot 4+0+1=81$
263 6p3e9 ${⊢}6+3=9$
264 16 15 41 103 263 decaddi ${⊢}4\cdot 4+3=19$
265 35 2 3 41 222 257 2 12 16 262 264 decmac ${⊢}204\cdot 4+3=819$
266 153 64 191 addcomli ${⊢}4+7=11$
267 20 2 28 95 232 16 266 decaddci ${⊢}6\cdot 4+7=31$
268 36 15 28 219 2 16 41 265 267 decrmac ${⊢}2046\cdot 4+7=8191$
269 35 2 220 28 222 223 37 16 225 256 268 decma2c ${⊢}2046\cdot 204+1227=418611$
270 50 mul02i ${⊢}0\cdot 6=0$
271 270 oveq1i ${⊢}0\cdot 6+2=0+2$
272 271 132 eqtri ${⊢}0\cdot 6+2=2$
273 20 3 20 226 15 53 272 decrmanc ${⊢}20\cdot 6+2=122$
274 4p3e7 ${⊢}4+3=7$
275 20 2 41 96 274 decaddi ${⊢}4\cdot 6+3=27$
276 35 2 41 222 15 28 20 273 275 decrmac ${⊢}204\cdot 6+3=1227$
277 15 36 15 219 15 41 276 90 decmul1c ${⊢}2046\cdot 6=12276$
278 37 36 15 219 15 221 269 277 decmul2c ${⊢}2046\cdot 2046=4186116$
279 218 278 eqtr4i ${⊢}1046\cdot {N}+1070=2046\cdot 2046$
280 8 9 31 34 37 30 178 183 279 mod2xi ${⊢}{2}^{50}\mathrm{mod}{N}=1070\mathrm{mod}{N}$
281 23 nn0cni ${⊢}50\in ℂ$
282 eqid ${⊢}50=50$
283 20 22 3 282 181 241 decmul1 ${⊢}50\cdot 2=100$
284 281 51 283 mulcomli ${⊢}2\cdot 50=100$
285 eqid ${⊢}614=614$
286 20 12 deccl ${⊢}29\in {ℕ}_{0}$
287 eqid ${⊢}61=61$
288 eqid ${⊢}29=29$
289 199 oveq1i ${⊢}6+2+1=8+1$
290 289 125 eqtri ${⊢}6+2+1=9$
291 15 16 20 12 287 288 290 148 decaddc2 ${⊢}61+29=90$
292 61 3 eqeltri ${⊢}0+0\in {ℕ}_{0}$
293 eqid ${⊢}286=286$
294 eqid ${⊢}28=28$
295 122 oveq1i ${⊢}2\cdot 4+3=8+3$
296 8p3e11 ${⊢}8+3=11$
297 295 296 eqtri ${⊢}2\cdot 4+3=11$
298 8t4e32 ${⊢}8\cdot 4=32$
299 41 20 20 298 88 decaddi ${⊢}8\cdot 4+2=34$
300 20 24 20 294 2 2 41 297 299 decrmac ${⊢}28\cdot 4+2=114$
301 95 61 oveq12i ${⊢}6\cdot 4+0+0=24+0$
302 38 nn0cni ${⊢}24\in ℂ$
303 302 addid1i ${⊢}24+0=24$
304 301 303 eqtri ${⊢}6\cdot 4+0+0=24$
305 25 15 292 293 2 2 20 300 304 decrmac ${⊢}286\cdot 4+0+0=1144$
306 26 nn0cni ${⊢}286\in ℂ$
307 306 mul01i ${⊢}286\cdot 0=0$
308 307 oveq1i ${⊢}286\cdot 0+9=0+9$
309 308 75 58 3eqtri ${⊢}286\cdot 0+9=09$
310 2 3 3 12 60 59 26 12 3 305 309 decma2c ${⊢}286\cdot 40+9+0=11449$
311 307 oveq1i ${⊢}286\cdot 0+0=0+0$
312 311 61 62 3eqtri ${⊢}286\cdot 0+0=00$
313 4 3 12 3 55 291 26 3 3 310 312 decma2c ${⊢}286\cdot 400+61+29=114490$
314 230 mulid1i ${⊢}8\cdot 1=8$
315 16 20 24 294 109 314 decmul1 ${⊢}28\cdot 1=28$
316 20 24 125 315 decsuc ${⊢}28\cdot 1+1=29$
317 50 mulid1i ${⊢}6\cdot 1=6$
318 317 oveq1i ${⊢}6\cdot 1+4=6+4$
319 318 92 eqtri ${⊢}6\cdot 1+4=10$
320 25 15 2 293 16 3 16 316 319 decrmac ${⊢}286\cdot 1+4=290$
321 5 16 17 2 1 285 26 3 286 313 320 decma2c ${⊢}286\cdot {N}+614=1144900$
322 16 16 deccl ${⊢}11\in {ℕ}_{0}$
323 322 2 deccl ${⊢}114\in {ℕ}_{0}$
324 323 2 deccl ${⊢}1144\in {ℕ}_{0}$
325 324 12 deccl ${⊢}11449\in {ℕ}_{0}$
326 28 2 deccl ${⊢}74\in {ℕ}_{0}$
327 326 12 deccl ${⊢}749\in {ℕ}_{0}$
328 eqid ${⊢}10=10$
329 eqid ${⊢}749=749$
330 326 nn0cni ${⊢}74\in ℂ$
331 330 addid1i ${⊢}74+0=74$
332 153 addid1i ${⊢}7+0=7$
333 332 28 eqeltri ${⊢}7+0\in {ℕ}_{0}$
334 10 nn0cni ${⊢}10\in ℂ$
335 334 mulid1i ${⊢}10\cdot 1=10$
336 16 3 188 335 decsuc ${⊢}10\cdot 1+1=11$
337 153 mulid1i ${⊢}7\cdot 1=7$
338 337 332 oveq12i ${⊢}7\cdot 1+7+0=7+7$
339 7p7e14 ${⊢}7+7=14$
340 338 339 eqtri ${⊢}7\cdot 1+7+0=14$
341 10 28 333 186 16 2 16 336 340 decrmac ${⊢}107\cdot 1+7+0=114$
342 69 mul02i ${⊢}0\cdot 1=0$
343 342 oveq1i ${⊢}0\cdot 1+4=0+4$
344 64 addid2i ${⊢}0+4=4$
345 343 344 114 3eqtri ${⊢}0\cdot 1+4=04$
346 29 3 28 2 184 331 16 2 3 341 345 decmac ${⊢}1070\cdot 1+74+0=1144$
347 30 nn0cni ${⊢}1070\in ℂ$
348 347 mul01i ${⊢}1070\cdot 0=0$
349 348 oveq1i ${⊢}1070\cdot 0+9=0+9$
350 349 75 58 3eqtri ${⊢}1070\cdot 0+9=09$
351 16 3 326 12 328 329 30 12 3 346 350 decma2c ${⊢}1070\cdot 10+749=11449$
352 dfdec10 ${⊢}74=10\cdot 7+4$
353 352 eqcomi ${⊢}10\cdot 7+4=74$
354 7t7e49 ${⊢}7\cdot 7=49$
355 28 10 28 186 12 2 353 354 decmul1c ${⊢}107\cdot 7=749$
356 153 mul02i ${⊢}0\cdot 7=0$
357 28 29 3 184 355 356 decmul1 ${⊢}1070\cdot 7=7490$
358 30 10 28 186 3 327 351 357 decmul2c ${⊢}1070\cdot 107=114490$
359 325 3 3 358 61 decaddi ${⊢}1070\cdot 107+0=114490$
360 348 62 eqtri ${⊢}1070\cdot 0=00$
361 30 29 3 184 3 3 359 360 decmul2c ${⊢}1070\cdot 1070=1144900$
362 321 361 eqtr4i ${⊢}286\cdot {N}+614=1070\cdot 1070$
363 8 9 23 27 30 18 280 284 362 mod2xi ${⊢}{2}^{100}\mathrm{mod}{N}=614\mathrm{mod}{N}$
364 11 nn0cni ${⊢}100\in ℂ$
365 eqid ${⊢}100=100$
366 20 10 3 365 173 241 decmul1 ${⊢}100\cdot 2=200$
367 364 51 366 mulcomli ${⊢}2\cdot 100=200$
368 eqid ${⊢}902=902$
369 eqid ${⊢}90=90$
370 12 3 12 369 75 decaddi ${⊢}90+9=99$
371 eqid ${⊢}94=94$
372 6p1e7 ${⊢}6+1=7$
373 9t4e36 ${⊢}9\cdot 4=36$
374 41 15 372 373 decsuc ${⊢}9\cdot 4+1=37$
375 103 61 oveq12i ${⊢}4\cdot 4+0+0=16+0$
376 16 15 deccl ${⊢}16\in {ℕ}_{0}$
377 376 nn0cni ${⊢}16\in ℂ$
378 377 addid1i ${⊢}16+0=16$
379 375 378 eqtri ${⊢}4\cdot 4+0+0=16$
380 12 2 292 371 2 15 16 374 379 decrmac ${⊢}94\cdot 4+0+0=376$
381 238 mul01i ${⊢}94\cdot 0=0$
382 381 oveq1i ${⊢}94\cdot 0+9=0+9$
383 382 75 58 3eqtri ${⊢}94\cdot 0+9=09$
384 2 3 3 12 60 59 13 12 3 380 383 decma2c ${⊢}94\cdot 40+9+0=3769$
385 4 3 12 12 55 370 13 12 3 384 383 decma2c ${⊢}94\cdot 400+90+9=37699$
386 56 mulid1i ${⊢}9\cdot 1=9$
387 64 mulid1i ${⊢}4\cdot 1=4$
388 387 oveq1i ${⊢}4\cdot 1+2=4+2$
389 388 203 eqtri ${⊢}4\cdot 1+2=6$
390 12 2 20 371 16 386 389 decrmanc ${⊢}94\cdot 1+2=96$
391 5 16 19 20 1 368 13 15 12 385 390 decma2c ${⊢}94\cdot {N}+902=376996$
392 38 22 deccl ${⊢}245\in {ℕ}_{0}$
393 eqid ${⊢}245=245$
394 50 51 199 addcomli ${⊢}2+6=8$
395 20 2 15 16 165 287 394 101 decadd ${⊢}24+61=85$
396 8p2e10 ${⊢}8+2=10$
397 41 15 372 90 decsuc ${⊢}6\cdot 6+1=37$
398 50 mulid2i ${⊢}1\cdot 6=6$
399 398 oveq1i ${⊢}1\cdot 6+0=6+0$
400 50 addid1i ${⊢}6+0=6$
401 399 400 eqtri ${⊢}1\cdot 6+0=6$
402 15 16 16 3 287 396 15 397 401 decma ${⊢}61\cdot 6+8+2=376$
403 17 2 24 22 285 395 15 12 20 402 99 decmac ${⊢}614\cdot 6+24+61=3769$
404 16 15 16 287 317 78 decmul1 ${⊢}61\cdot 1=61$
405 387 oveq1i ${⊢}4\cdot 1+5=4+5$
406 405 98 eqtri ${⊢}4\cdot 1+5=9$
407 17 2 22 285 16 404 406 decrmanc ${⊢}614\cdot 1+5=619$
408 15 16 38 22 287 393 18 12 17 403 407 decma2c ${⊢}614\cdot 61+245=37699$
409 65 oveq1i ${⊢}1\cdot 4+1=4+1$
410 409 101 eqtri ${⊢}1\cdot 4+1=5$
411 15 16 16 287 2 95 410 decrmanc ${⊢}61\cdot 4+1=245$
412 2 17 2 285 15 16 411 103 decmul1c ${⊢}614\cdot 4=2456$
413 18 17 2 285 15 392 408 412 decmul2c ${⊢}614\cdot 614=376996$
414 391 413 eqtr4i ${⊢}94\cdot {N}+902=614\cdot 614$
415 8 9 11 14 18 21 363 367 414 mod2xi ${⊢}{2}^{200}\mathrm{mod}{N}=902\mathrm{mod}{N}$