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	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 \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	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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+1023=9025$$
143	2 28	deccl	$$⊢47\in {\mathbb{N}}_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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+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 \mathrm{<mi\; mathcolor="\#808">N</mi>}=0$$
171	170	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+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 {\mathbb{N}}_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 {\mathbb{N}}_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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+1070=4186116$$
219		eqid	$$⊢2046=2046$$
220	43 20	deccl	$$⊢122\in {\mathbb{N}}_0$$
221	220 28	deccl	$$⊢1227\in {\mathbb{N}}_0$$
222		eqid	$$⊢204=204$$
223		eqid	$$⊢1227=1227$$
224	24 16	deccl	$$⊢81\in {\mathbb{N}}_0$$
225	224 12	deccl	$$⊢819\in {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+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 {\mathbb{N}}_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 {\mathbb{N}}_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 \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	addid1i	$$⊢74+0=74$$
332	153	addid1i	$$⊢7+0=7$$
333	332 28	eqeltri	$$⊢7+0\in {\mathbb{N}}_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 \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 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 {\mathbb{N}}_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 \mathrm{<mi\; mathcolor="\#808">N</mi>}+902=376996$$
392	38 22	deccl	$$⊢245\in {\mathbb{N}}_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 \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$$