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 {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢40\in {\mathbb{N}}_0$$
5	4 3	deccl	$$⊢400\in {\mathbb{N}}_0$$
6		1nn	$$⊢1\in \mathbb{N}$$
7	5 6	decnncl	$$⊢4001\in \mathbb{N}$$
8	1 7	eqeltri	$$⊢N\in \mathbb{N}$$
9		2nn	$$⊢2\in \mathbb{N}$$
10		10nn0	$$⊢10\in {\mathbb{N}}_0$$
11	10 3	deccl	$$⊢100\in {\mathbb{N}}_0$$
12		9nn0	$$⊢9\in {\mathbb{N}}_0$$
13	12 2	deccl	$$⊢94\in {\mathbb{N}}_0$$
14	13	nn0zi	$$⊢94\in \mathbb{Z}$$
15		6nn0	$$⊢6\in {\mathbb{N}}_0$$
16		1nn0	$$⊢1\in {\mathbb{N}}_0$$
17	15 16	deccl	$$⊢61\in {\mathbb{N}}_0$$
18	17 2	deccl	$$⊢614\in {\mathbb{N}}_0$$
19	12 3	deccl	$$⊢90\in {\mathbb{N}}_0$$
20		2nn0	$$⊢2\in {\mathbb{N}}_0$$
21	19 20	deccl	$$⊢902\in {\mathbb{N}}_0$$
22		5nn0	$$⊢5\in {\mathbb{N}}_0$$
23	22 3	deccl	$$⊢50\in {\mathbb{N}}_0$$
24		8nn0	$$⊢8\in {\mathbb{N}}_0$$
25	20 24	deccl	$$⊢28\in {\mathbb{N}}_0$$
26	25 15	deccl	$$⊢286\in {\mathbb{N}}_0$$
27	26	nn0zi	$$⊢286\in \mathbb{Z}$$
28		7nn0	$$⊢7\in {\mathbb{N}}_0$$
29	10 28	deccl	$$⊢107\in {\mathbb{N}}_0$$
30	29 3	deccl	$$⊢1070\in {\mathbb{N}}_0$$
31	20 22	deccl	$$⊢25\in {\mathbb{N}}_0$$
32	10 2	deccl	$$⊢104\in {\mathbb{N}}_0$$
33	32 15	deccl	$$⊢1046\in {\mathbb{N}}_0$$
34	33	nn0zi	$$⊢1046\in \mathbb{Z}$$
35	20 3	deccl	$$⊢20\in {\mathbb{N}}_0$$
36	35 2	deccl	$$⊢204\in {\mathbb{N}}_0$$
37	36 15	deccl	$$⊢2046\in {\mathbb{N}}_0$$
38	20 2	deccl	$$⊢24\in {\mathbb{N}}_0$$
39		0z	$$⊢0\in \mathbb{Z}$$
40	10 20	deccl	$$⊢102\in {\mathbb{N}}_0$$
41		3nn0	$$⊢3\in {\mathbb{N}}_0$$
42	40 41	deccl	$$⊢1023\in {\mathbb{N}}_0$$
43	16 20	deccl	$$⊢12\in {\mathbb{N}}_0$$
44		2z	$$⊢2\in \mathbb{Z}$$
45	12 22	deccl	$$⊢95\in {\mathbb{N}}_0$$
46		1z	$$⊢1\in \mathbb{Z}$$
47	15 2	deccl	$$⊢64\in {\mathbb{N}}_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	addridi	$$⊢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	mullidi	$$⊢1\cdot 4=4$$
66	65 61	oveq12i	$$⊢1\cdot 4+0+0=4+0$$
67	64	addridi	$$⊢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	addlidi	$$⊢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	mulridi	$$⊢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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+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	mulridi	$$⊢2\cdot 1=2$$
110	109	oveq1i	$$⊢2\cdot 1+0=2+0$$
111	51	addridi	$$⊢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	addridi	$$⊢102+0=102$$
120		dec10p	$$⊢10+0=10$$
121		2t4e8	$$⊢2\cdot 4=8$$
122	69	addridi	$$⊢1+0=1$$
123	121 122	oveq12i	$$⊢2\cdot 4+1+0=8+1$$
124		8p1e9	$$⊢8+1=9$$
125	123 124	eqtri	$$⊢2\cdot 4+1+0=9$$
126	51	mul01i	$$⊢2\cdot 0=0$$
127	126	oveq1i	$$⊢2\cdot 0+0=0+0$$
128	127 61 62	3eqtri	$$⊢2\cdot 0+0=00$$
129	2 3 16 3 60 120 20 3 3 125 128	decma2c	$$⊢2\cdot 40+10+0=90$$
130	126	oveq1i	$$⊢2\cdot 0+2=0+2$$
131	51	addlidi	$$⊢0+2=2$$
132	20	dec0h	$$⊢2=02$$
133	130 131 132	3eqtri	$$⊢2\cdot 0+2=02$$
134	4 3 10 20 55 119 20 20 3 129 133	decma2c	$$⊢2\cdot 400+102+0=902$$
135	109	oveq1i	$$⊢2\cdot 1+3=2+3$$
136		3cn	$$⊢3\in ℂ$$
137		3p2e5	$$⊢3+2=5$$
138	136 51 137	addcomli	$$⊢2+3=5$$
139	22	dec0h	$$⊢5=05$$
140	135 138 139	3eqtri	$$⊢2\cdot 1+3=05$$
141	5 16 40 41 1 117 20 22 3 134 140	decma2c	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1023=9025$$
142	2 28	deccl	$$⊢47\in {\mathbb{N}}_0$$
143		eqid	$$⊢47=47$$
144	98	oveq2i	$$⊢9\cdot 9+4+5=9\cdot 9+9$$
145		9t9e81	$$⊢9\cdot 9=81$$
146		9p1e10	$$⊢9+1=10$$
147	56 69 146	addcomli	$$⊢1+9=10$$
148	24 16 12 145 124 147	decaddci2	$$⊢9\cdot 9+9=90$$
149	144 148	eqtri	$$⊢9\cdot 9+4+5=90$$
150		9t5e45	$$⊢9\cdot 5=45$$
151	56 80 150	mulcomli	$$⊢5\cdot 9=45$$
152		7cn	$$⊢7\in ℂ$$
153		7p5e12	$$⊢7+5=12$$
154	152 80 153	addcomli	$$⊢5+7=12$$
155	2 22 28 151 101 20 154	decaddci	$$⊢5\cdot 9+7=52$$
156	12 22 2 28 54 143 12 20 22 149 155	decmac	$$⊢95\cdot 9+47=902$$
157		5p2e7	$$⊢5+2=7$$
158	2 22 20 150 157	decaddi	$$⊢9\cdot 5+2=47$$
159		5t5e25	$$⊢5\cdot 5=25$$
160	22 12 22 54 22 20 158 159	decmul1c	$$⊢95\cdot 5=475$$
161	45 12 22 54 22 142 156 160	decmul2c	$$⊢95\cdot 95=9025$$
162	141 161	eqtr4i	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1023=95\cdot 95$$
163	8 9 43 44 45 42 107 116 162	mod2xi	$$⊢2^{24}\mathrm{mod}N=1023\mathrm{mod}N$$
164		eqid	$$⊢24=24$$
165	20 2 101 164	decsuc	$$⊢24+1=25$$
166	37	nn0cni	$$⊢2046\in ℂ$$
167	166	addlidi	$$⊢0+2046=2046$$
168	8	nncni	$$⊢N\in ℂ$$
169	168	mul02i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0$$
170	169	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2046=0+2046$$
171		eqid	$$⊢102=102$$
172	20	dec0u	$$⊢10\cdot 2=20$$
173	20 10 20 171 172 113	decmul1	$$⊢102\cdot 2=204$$
174		3t2e6	$$⊢3\cdot 2=6$$
175	20 40 41 117 173 174	decmul1	$$⊢1023\cdot 2=2046$$
176	167 170 175	3eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2046=1023\cdot 2$$
177	8 9 38 39 42 37 163 165 176	modxp1i	$$⊢2^{25}\mathrm{mod}N=2046\mathrm{mod}N$$
178	113	oveq1i	$$⊢2\cdot 2+1=4+1$$
179	178 101	eqtri	$$⊢2\cdot 2+1=5$$
180		5t2e10	$$⊢5\cdot 2=10$$
181	80 51 180	mulcomli	$$⊢2\cdot 5=10$$
182	20 20 22 87 3 16 179 181	decmul2c	$$⊢2\cdot 25=50$$
183		eqid	$$⊢1070=1070$$
184	20 16	deccl	$$⊢21\in {\mathbb{N}}_0$$
185		eqid	$$⊢107=107$$
186		eqid	$$⊢104=104$$
187		0p1e1	$$⊢0+1=1$$
188		10p10e20	$$⊢10+10=20$$
189	20 3 187 188	decsuc	$$⊢10+10+1=21$$
190		7p4e11	$$⊢7+4=11$$
191	10 28 10 2 185 186 189 16 190	decaddc	$$⊢107+104=211$$
192	184	nn0cni	$$⊢21\in ℂ$$
193	192	addridi	$$⊢21+0=21$$
194	111 20	eqeltri	$$⊢2+0\in {\mathbb{N}}_0$$
195		eqid	$$⊢1046=1046$$
196		dfdec10	$$⊢41=10\cdot 4+1$$
197	196	eqcomi	$$⊢10\cdot 4+1=41$$
198		6p2e8	$$⊢6+2=8$$
199	16 15 20 103 198	decaddi	$$⊢4\cdot 4+2=18$$
200	10 2 20 186 2 24 16 197 199	decrmac	$$⊢104\cdot 4+2=418$$
201	95 111	oveq12i	$$⊢6\cdot 4+2+0=24+2$$
202		4p2e6	$$⊢4+2=6$$
203	20 2 20 164 202	decaddi	$$⊢24+2=26$$
204	201 203	eqtri	$$⊢6\cdot 4+2+0=26$$
205	32 15 194 195 2 15 20 200 204	decrmac	$$⊢1046\cdot 4+2+0=4186$$
206	33	nn0cni	$$⊢1046\in ℂ$$
207	206	mul01i	$$⊢1046\cdot 0=0$$
208	207	oveq1i	$$⊢1046\cdot 0+1=0+1$$
209	16	dec0h	$$⊢1=01$$
210	208 187 209	3eqtri	$$⊢1046\cdot 0+1=01$$
211	2 3 20 16 60 193 33 16 3 205 210	decma2c	$$⊢1046\cdot 40+21+0=41861$$
212	4 3 184 16 55 191 33 16 3 211 210	decma2c	$$⊢1046\cdot 400+107+104=418611$$
213	206	mulridi	$$⊢1046\cdot 1=1046$$
214	213	oveq1i	$$⊢1046\cdot 1+0=1046+0$$
215	206	addridi	$$⊢1046+0=1046$$
216	214 215	eqtri	$$⊢1046\cdot 1+0=1046$$
217	5 16 29 3 1 183 33 15 32 212 216	decma2c	$$⊢1046\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1070=4186116$$
218		eqid	$$⊢2046=2046$$
219	43 20	deccl	$$⊢122\in {\mathbb{N}}_0$$
220	219 28	deccl	$$⊢1227\in {\mathbb{N}}_0$$
221		eqid	$$⊢204=204$$
222		eqid	$$⊢1227=1227$$
223	24 16	deccl	$$⊢81\in {\mathbb{N}}_0$$
224	223 12	deccl	$$⊢819\in {\mathbb{N}}_0$$
225		eqid	$$⊢20=20$$
226		eqid	$$⊢122=122$$
227		eqid	$$⊢819=819$$
228		eqid	$$⊢81=81$$
229		8cn	$$⊢8\in ℂ$$
230	229 69 124	addcomli	$$⊢1+8=9$$
231		2p1e3	$$⊢2+1=3$$
232	16 20 24 16 108 228 230 231	decadd	$$⊢12+81=93$$
233	12 41 91 232	decsuc	$$⊢12+81+1=94$$
234		9p2e11	$$⊢9+2=11$$
235	56 51 234	addcomli	$$⊢2+9=11$$
236	43 20 223 12 226 227 233 16 235	decaddc	$$⊢122+819=941$$
237	13	nn0cni	$$⊢94\in ℂ$$
238	237	addridi	$$⊢94+0=94$$
239	122 16	eqeltri	$$⊢1+0\in {\mathbb{N}}_0$$
240	51	mul02i	$$⊢0\cdot 2=0$$
241	240 122	oveq12i	$$⊢0\cdot 2+1+0=0+1$$
242	241 187	eqtri	$$⊢0\cdot 2+1+0=1$$
243	20 3 239 225 20 113 242	decrmanc	$$⊢20\cdot 2+1+0=41$$
244		4t2e8	$$⊢4\cdot 2=8$$
245	244	oveq1i	$$⊢4\cdot 2+0=8+0$$
246	229	addridi	$$⊢8+0=8$$
247	24	dec0h	$$⊢8=08$$
248	245 246 247	3eqtri	$$⊢4\cdot 2+0=08$$
249	35 2 16 3 221 146 20 24 3 243 248	decmac	$$⊢204\cdot 2+9+1=418$$
250	64 51 202	addcomli	$$⊢2+4=6$$
251	16 20 2 52 250	decaddi	$$⊢6\cdot 2+4=16$$
252	36 15 12 2 218 238 20 15 16 249 251	decmac	$$⊢2046\cdot 2+94+0=4186$$
253	166	mul01i	$$⊢2046\cdot 0=0$$
254	253	oveq1i	$$⊢2046\cdot 0+1=0+1$$
255	254 187 209	3eqtri	$$⊢2046\cdot 0+1=01$$
256	20 3 13 16 225 236 37 16 3 252 255	decma2c	$$⊢2046\cdot 20+122+819=41861$$
257	41	dec0h	$$⊢3=03$$
258	187 16	eqeltri	$$⊢0+1\in {\mathbb{N}}_0$$
259	64	mul02i	$$⊢0\cdot 4=0$$
260	259 187	oveq12i	$$⊢0\cdot 4+0+1=0+1$$
261	260 187	eqtri	$$⊢0\cdot 4+0+1=1$$
262	20 3 258 225 2 121 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 221 257 2 12 16 262 264	decmac	$$⊢204\cdot 4+3=819$$
266	152 64 190	addcomli	$$⊢4+7=11$$
267	20 2 28 95 231 16 266	decaddci	$$⊢6\cdot 4+7=31$$
268	36 15 28 218 2 16 41 265 267	decrmac	$$⊢2046\cdot 4+7=8191$$
269	35 2 219 28 221 222 37 16 224 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 131	eqtri	$$⊢0\cdot 6+2=2$$
273	20 3 20 225 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 221 15 28 20 273 275	decrmac	$$⊢204\cdot 6+3=1227$$
277	15 36 15 218 15 41 276 90	decmul1c	$$⊢2046\cdot 6=12276$$
278	37 36 15 218 15 220 269 277	decmul2c	$$⊢2046\cdot 2046=4186116$$
279	217 278	eqtr4i	$$⊢1046\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1070=2046\cdot 2046$$
280	8 9 31 34 37 30 177 182 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 180 240	decmul1	$$⊢50\cdot 2=100$$
284	281 51 283	mulcomli	$$⊢2\cdot 50=100$$
285		eqid	$$⊢614=614$$
286	20 12	deccl	$$⊢29\in {\mathbb{N}}_0$$
287		eqid	$$⊢61=61$$
288		eqid	$$⊢29=29$$
289	198	oveq1i	$$⊢6+2+1=8+1$$
290	289 124	eqtri	$$⊢6+2+1=9$$
291	15 16 20 12 287 288 290 147	decaddc2	$$⊢61+29=90$$
292	61 3	eqeltri	$$⊢0+0\in {\mathbb{N}}_0$$
293		eqid	$$⊢286=286$$
294		eqid	$$⊢28=28$$
295	121	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	addridi	$$⊢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	229	mulridi	$$⊢8\cdot 1=8$$
315	16 20 24 294 109 314	decmul1	$$⊢28\cdot 1=28$$
316	20 24 124 315	decsuc	$$⊢28\cdot 1+1=29$$
317	50	mulridi	$$⊢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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+614=1144900$$
322	16 16	deccl	$$⊢11\in {\mathbb{N}}_0$$
323	322 2	deccl	$$⊢114\in {\mathbb{N}}_0$$
324	323 2	deccl	$$⊢1144\in {\mathbb{N}}_0$$
325	324 12	deccl	$$⊢11449\in {\mathbb{N}}_0$$
326	28 2	deccl	$$⊢74\in {\mathbb{N}}_0$$
327	326 12	deccl	$$⊢749\in {\mathbb{N}}_0$$
328		eqid	$$⊢10=10$$
329		eqid	$$⊢749=749$$
330	326	nn0cni	$$⊢74\in ℂ$$
331	330	addridi	$$⊢74+0=74$$
332	152	addridi	$$⊢7+0=7$$
333	332 28	eqeltri	$$⊢7+0\in {\mathbb{N}}_0$$
334	10	nn0cni	$$⊢10\in ℂ$$
335	334	mulridi	$$⊢10\cdot 1=10$$
336	16 3 187 335	decsuc	$$⊢10\cdot 1+1=11$$
337	152	mulridi	$$⊢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 185 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	addlidi	$$⊢0+4=4$$
345	343 344 114	3eqtri	$$⊢0\cdot 1+4=04$$
346	29 3 28 2 183 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 185 12 2 353 354	decmul1c	$$⊢107\cdot 7=749$$
356	152	mul02i	$$⊢0\cdot 7=0$$
357	28 29 3 183 355 356	decmul1	$$⊢1070\cdot 7=7490$$
358	30 10 28 185 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 183 3 3 359 360	decmul2c	$$⊢1070\cdot 1070=1144900$$
362	321 361	eqtr4i	$$⊢286\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+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 172 240	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 {\mathbb{N}}_0$$
377	376	nn0cni	$$⊢16\in ℂ$$
378	377	addridi	$$⊢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	237	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	mulridi	$$⊢9\cdot 1=9$$
387	64	mulridi	$$⊢4\cdot 1=4$$
388	387	oveq1i	$$⊢4\cdot 1+2=4+2$$
389	388 202	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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+902=376996$$
392	38 22	deccl	$$⊢245\in {\mathbb{N}}_0$$
393		eqid	$$⊢245=245$$
394	50 51 198	addcomli	$$⊢2+6=8$$
395	20 2 15 16 164 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	mullidi	$$⊢1\cdot 6=6$$
399	398	oveq1i	$$⊢1\cdot 6+0=6+0$$
400	50	addridi	$$⊢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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+902=614\cdot 614$$
415	8 9 11 14 18 21 363 367 414	mod2xi	$$⊢2^{200}\mathrm{mod}N=902\mathrm{mod}N$$