Theorem 2503lem2

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

	Ref	Expression
Hypothesis	2503prm.1	$$⊢N=2503$$
Assertion	2503lem2	$$⊢2^{N-1}\mathrm{mod}N=1\mathrm{mod}N$$

Proof

Step	Hyp	Ref	Expression
1		2503prm.1	$$⊢N=2503$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		5nn0	$$⊢5\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢25\in {\mathbb{N}}_0$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	4 5	deccl	$$⊢250\in {\mathbb{N}}_0$$
7		3nn	$$⊢3\in \mathbb{N}$$
8	6 7	decnncl	$$⊢2503\in \mathbb{N}$$
9	1 8	eqeltri	$$⊢N\in \mathbb{N}$$
10		2nn	$$⊢2\in \mathbb{N}$$
11		1nn0	$$⊢1\in {\mathbb{N}}_0$$
12	11 2	deccl	$$⊢12\in {\mathbb{N}}_0$$
13	12 3	deccl	$$⊢125\in {\mathbb{N}}_0$$
14	13 11	deccl	$$⊢1251\in {\mathbb{N}}_0$$
15		0z	$$⊢0\in \mathbb{Z}$$
16		4nn0	$$⊢4\in {\mathbb{N}}_0$$
17	12 16	deccl	$$⊢124\in {\mathbb{N}}_0$$
18		8nn0	$$⊢8\in {\mathbb{N}}_0$$
19	17 18	deccl	$$⊢1248\in {\mathbb{N}}_0$$
20		1z	$$⊢1\in \mathbb{Z}$$
21		3nn0	$$⊢3\in {\mathbb{N}}_0$$
22	21 11	deccl	$$⊢31\in {\mathbb{N}}_0$$
23	22 21	deccl	$$⊢313\in {\mathbb{N}}_0$$
24		6nn0	$$⊢6\in {\mathbb{N}}_0$$
25	24 2	deccl	$$⊢62\in {\mathbb{N}}_0$$
26	25 16	deccl	$$⊢624\in {\mathbb{N}}_0$$
27		9nn0	$$⊢9\in {\mathbb{N}}_0$$
28	2 27	deccl	$$⊢29\in {\mathbb{N}}_0$$
29	28	nn0zi	$$⊢29\in \mathbb{Z}$$
30		7nn0	$$⊢7\in {\mathbb{N}}_0$$
31	2 30	deccl	$$⊢27\in {\mathbb{N}}_0$$
32	31 5	deccl	$$⊢270\in {\mathbb{N}}_0$$
33	22 2	deccl	$$⊢312\in {\mathbb{N}}_0$$
34	2 21	deccl	$$⊢23\in {\mathbb{N}}_0$$
35	34 18	deccl	$$⊢238\in {\mathbb{N}}_0$$
36	35	nn0zi	$$⊢238\in \mathbb{Z}$$
37	30 30	deccl	$$⊢77\in {\mathbb{N}}_0$$
38	37 2	deccl	$$⊢772\in {\mathbb{N}}_0$$
39	11 3	deccl	$$⊢15\in {\mathbb{N}}_0$$
40	39 24	deccl	$$⊢156\in {\mathbb{N}}_0$$
41	21	nn0zi	$$⊢3\in \mathbb{Z}$$
42	27 11	deccl	$$⊢91\in {\mathbb{N}}_0$$
43	30 18	deccl	$$⊢78\in {\mathbb{N}}_0$$
44	39	nn0zi	$$⊢15\in \mathbb{Z}$$
45	11 27	deccl	$$⊢19\in {\mathbb{N}}_0$$
46		4nn	$$⊢4\in \mathbb{N}$$
47	45 46	decnncl	$$⊢194\in \mathbb{N}$$
48	34 5	deccl	$$⊢230\in {\mathbb{N}}_0$$
49	48 27	deccl	$$⊢2309\in {\mathbb{N}}_0$$
50	21 27	deccl	$$⊢39\in {\mathbb{N}}_0$$
51	16	nn0zi	$$⊢4\in \mathbb{Z}$$
52	11 11	deccl	$$⊢11\in {\mathbb{N}}_0$$
53	52 11	deccl	$$⊢111\in {\mathbb{N}}_0$$
54	21 18	deccl	$$⊢38\in {\mathbb{N}}_0$$
55	11 21	deccl	$$⊢13\in {\mathbb{N}}_0$$
56	55 5	deccl	$$⊢130\in {\mathbb{N}}_0$$
57	56 30	deccl	$$⊢1307\in {\mathbb{N}}_0$$
58	3 21	deccl	$$⊢53\in {\mathbb{N}}_0$$
59	58 18	deccl	$$⊢538\in {\mathbb{N}}_0$$
60	59	nn0zi	$$⊢538\in \mathbb{Z}$$
61	52 24	deccl	$$⊢116\in {\mathbb{N}}_0$$
62	61 11	deccl	$$⊢1161\in {\mathbb{N}}_0$$
63	11 18	deccl	$$⊢18\in {\mathbb{N}}_0$$
64	63 21	deccl	$$⊢183\in {\mathbb{N}}_0$$
65	64 2	deccl	$$⊢1832\in {\mathbb{N}}_0$$
66	1	2503lem1	$$⊢2^{18}\mathrm{mod}N=1832\mathrm{mod}N$$
67		8p1e9	$$⊢8+1=9$$
68		eqid	$$⊢18=18$$
69	11 18 67 68	decsuc	$$⊢18+1=19$$
70		eqid	$$⊢1161=1161$$
71		eqid	$$⊢250=250$$
72	61	nn0cni	$$⊢116\in ℂ$$
73	72	addridi	$$⊢116+0=116$$
74		eqid	$$⊢25=25$$
75	52	nn0cni	$$⊢11\in ℂ$$
76	75	addridi	$$⊢11+0=11$$
77		2cn	$$⊢2\in ℂ$$
78	77	mullidi	$$⊢1\cdot 2=2$$
79		1p0e1	$$⊢1+0=1$$
80	78 79	oveq12i	$$⊢1\cdot 2+1+0=2+1$$
81		2p1e3	$$⊢2+1=3$$
82	80 81	eqtri	$$⊢1\cdot 2+1+0=3$$
83		5cn	$$⊢5\in ℂ$$
84	83	mullidi	$$⊢1\cdot 5=5$$
85	84	oveq1i	$$⊢1\cdot 5+1=5+1$$
86		5p1e6	$$⊢5+1=6$$
87	24	dec0h	$$⊢6=06$$
88	85 86 87	3eqtri	$$⊢1\cdot 5+1=06$$
89	2 3 11 11 74 76 11 24 5 82 88	decma2c	$$⊢1\cdot 25+11+0=36$$
90		ax-1cn	$$⊢1\in ℂ$$
91	90	mul01i	$$⊢1\cdot 0=0$$
92	91	oveq1i	$$⊢1\cdot 0+6=0+6$$
93		6cn	$$⊢6\in ℂ$$
94	93	addlidi	$$⊢0+6=6$$
95	92 94 87	3eqtri	$$⊢1\cdot 0+6=06$$
96	4 5 52 24 71 73 11 24 5 89 95	decma2c	$$⊢1\cdot 250+116+0=366$$
97		3cn	$$⊢3\in ℂ$$
98	97	mullidi	$$⊢1\cdot 3=3$$
99	98	oveq1i	$$⊢1\cdot 3+1=3+1$$
100		3p1e4	$$⊢3+1=4$$
101	16	dec0h	$$⊢4=04$$
102	99 100 101	3eqtri	$$⊢1\cdot 3+1=04$$
103	6 21 61 11 1 70 11 16 5 96 102	decma2c	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1161=3664$$
104		eqid	$$⊢1832=1832$$
105		eqid	$$⊢183=183$$
106	78	oveq1i	$$⊢1\cdot 2+1=2+1$$
107	106 81	eqtri	$$⊢1\cdot 2+1=3$$
108		8t2e16	$$⊢8\cdot 2=16$$
109	2 11 18 68 24 11 107 108	decmul1c	$$⊢18\cdot 2=36$$
110		3t2e6	$$⊢3\cdot 2=6$$
111	2 63 21 105 109 110	decmul1	$$⊢183\cdot 2=366$$
112		2t2e4	$$⊢2\cdot 2=4$$
113	2 64 2 104 111 112	decmul1	$$⊢1832\cdot 2=3664$$
114	103 113	eqtr4i	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1161=1832\cdot 2$$
115	9 10 63 20 65 62 66 69 114	modxp1i	$$⊢2^{19}\mathrm{mod}N=1161\mathrm{mod}N$$
116		eqid	$$⊢19=19$$
117		2t1e2	$$⊢2\cdot 1=2$$
118	117	oveq1i	$$⊢2\cdot 1+1=2+1$$
119	118 81	eqtri	$$⊢2\cdot 1+1=3$$
120		9cn	$$⊢9\in ℂ$$
121		9t2e18	$$⊢9\cdot 2=18$$
122	120 77 121	mulcomli	$$⊢2\cdot 9=18$$
123	2 11 27 116 18 11 119 122	decmul2c	$$⊢2\cdot 19=38$$
124		eqid	$$⊢1307=1307$$
125	11 24	deccl	$$⊢16\in {\mathbb{N}}_0$$
126	125 2	deccl	$$⊢162\in {\mathbb{N}}_0$$
127		eqid	$$⊢130=130$$
128		eqid	$$⊢162=162$$
129		eqid	$$⊢13=13$$
130		eqid	$$⊢16=16$$
131		1p1e2	$$⊢1+1=2$$
132		6p3e9	$$⊢6+3=9$$
133	93 97 132	addcomli	$$⊢3+6=9$$
134	11 21 11 24 129 130 131 133	decadd	$$⊢13+16=29$$
135	77	addlidi	$$⊢0+2=2$$
136	55 5 125 2 127 128 134 135	decadd	$$⊢130+162=292$$
137	28	nn0cni	$$⊢29\in ℂ$$
138	137	addridi	$$⊢29+0=29$$
139	2 24	deccl	$$⊢26\in {\mathbb{N}}_0$$
140	139 27	deccl	$$⊢269\in {\mathbb{N}}_0$$
141		eqid	$$⊢538=538$$
142	2	dec0h	$$⊢2=02$$
143		eqid	$$⊢269=269$$
144		6p1e7	$$⊢6+1=7$$
145	139	nn0cni	$$⊢26\in ℂ$$
146	145	addlidi	$$⊢0+26=26$$
147	2 24 144 146	decsuc	$$⊢0+26+1=27$$
148		9p2e11	$$⊢9+2=11$$
149	120 77 148	addcomli	$$⊢2+9=11$$
150	5 2 139 27 142 143 147 11 149	decaddc	$$⊢2+269=271$$
151		eqid	$$⊢53=53$$
152		7p1e8	$$⊢7+1=8$$
153		eqid	$$⊢27=27$$
154	2 30 152 153	decsuc	$$⊢27+1=28$$
155	81	oveq2i	$$⊢5\cdot 2+2+1=5\cdot 2+3$$
156		5t2e10	$$⊢5\cdot 2=10$$
157	97	addlidi	$$⊢0+3=3$$
158	11 5 21 156 157	decaddi	$$⊢5\cdot 2+3=13$$
159	155 158	eqtri	$$⊢5\cdot 2+2+1=13$$
160	110	oveq1i	$$⊢3\cdot 2+8=6+8$$
161		8cn	$$⊢8\in ℂ$$
162		8p6e14	$$⊢8+6=14$$
163	161 93 162	addcomli	$$⊢6+8=14$$
164	160 163	eqtri	$$⊢3\cdot 2+8=14$$
165	3 21 2 18 151 154 2 16 11 159 164	decmac	$$⊢53\cdot 2+27+1=134$$
166	11 24 144 108	decsuc	$$⊢8\cdot 2+1=17$$
167	58 18 31 11 141 150 2 30 11 165 166	decmac	$$⊢538\cdot 2+2+269=1347$$
168	27	dec0h	$$⊢9=09$$
169		4cn	$$⊢4\in ℂ$$
170	169	addlidi	$$⊢0+4=4$$
171	170 101	eqtri	$$⊢0+4=04$$
172		0p1e1	$$⊢0+1=1$$
173	172	oveq2i	$$⊢5\cdot 5+0+1=5\cdot 5+1$$
174		5t5e25	$$⊢5\cdot 5=25$$
175	2 3 86 174	decsuc	$$⊢5\cdot 5+1=26$$
176	173 175	eqtri	$$⊢5\cdot 5+0+1=26$$
177		5t3e15	$$⊢5\cdot 3=15$$
178	83 97 177	mulcomli	$$⊢3\cdot 5=15$$
179		5p4e9	$$⊢5+4=9$$
180	11 3 16 178 179	decaddi	$$⊢3\cdot 5+4=19$$
181	3 21 5 16 151 171 3 27 11 176 180	decmac	$$⊢53\cdot 5+0+4=269$$
182		8t5e40	$$⊢8\cdot 5=40$$
183	120	addlidi	$$⊢0+9=9$$
184	16 5 27 182 183	decaddi	$$⊢8\cdot 5+9=49$$
185	58 18 5 27 141 168 3 27 16 181 184	decmac	$$⊢538\cdot 5+9=2699$$
186	2 3 2 27 74 138 59 27 140 167 185	decma2c	$$⊢538\cdot 25+29+0=13479$$
187	59	nn0cni	$$⊢538\in ℂ$$
188	187	mul01i	$$⊢538\cdot 0=0$$
189	188	oveq1i	$$⊢538\cdot 0+2=0+2$$
190	189 135 142	3eqtri	$$⊢538\cdot 0+2=02$$
191	4 5 28 2 71 136 59 2 5 186 190	decma2c	$$⊢538\cdot 250+130+162=134792$$
192	30	dec0h	$$⊢7=07$$
193	21	dec0h	$$⊢3=03$$
194	157 193	eqtri	$$⊢0+3=03$$
195	172	oveq2i	$$⊢5\cdot 3+0+1=5\cdot 3+1$$
196	11 3 86 177	decsuc	$$⊢5\cdot 3+1=16$$
197	195 196	eqtri	$$⊢5\cdot 3+0+1=16$$
198		3t3e9	$$⊢3\cdot 3=9$$
199	198	oveq1i	$$⊢3\cdot 3+3=9+3$$
200		9p3e12	$$⊢9+3=12$$
201	199 200	eqtri	$$⊢3\cdot 3+3=12$$
202	3 21 5 21 151 194 21 2 11 197 201	decmac	$$⊢53\cdot 3+0+3=162$$
203		8t3e24	$$⊢8\cdot 3=24$$
204		7cn	$$⊢7\in ℂ$$
205		7p4e11	$$⊢7+4=11$$
206	204 169 205	addcomli	$$⊢4+7=11$$
207	2 16 30 203 81 11 206	decaddci	$$⊢8\cdot 3+7=31$$
208	58 18 5 30 141 192 21 11 21 202 207	decmac	$$⊢538\cdot 3+7=1621$$
209	6 21 56 30 1 124 59 11 126 191 208	decma2c	$$⊢538\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1307=1347921$$
210		eqid	$$⊢116=116$$
211	24 27	deccl	$$⊢69\in {\mathbb{N}}_0$$
212	211 30	deccl	$$⊢697\in {\mathbb{N}}_0$$
213	30 5	deccl	$$⊢70\in {\mathbb{N}}_0$$
214		eqid	$$⊢11=11$$
215		eqid	$$⊢697=697$$
216	11	dec0h	$$⊢1=01$$
217		eqid	$$⊢69=69$$
218	94	oveq1i	$$⊢0+6+1=6+1$$
219	218 144	eqtri	$$⊢0+6+1=7$$
220		9p1e10	$$⊢9+1=10$$
221	120 90 220	addcomli	$$⊢1+9=10$$
222	5 11 24 27 216 217 219 221	decaddc2	$$⊢1+69=70$$
223	204 90 152	addcomli	$$⊢1+7=8$$
224	11 11 211 30 214 215 222 223	decadd	$$⊢11+697=708$$
225		eqid	$$⊢70=70$$
226	5 30 11 11 192 214 172 152	decadd	$$⊢7+11=18$$
227	30 5 52 24 225 210 226 94	decadd	$$⊢70+116=186$$
228	63	nn0cni	$$⊢18\in ℂ$$
229	228	addridi	$$⊢18+0=18$$
230	131 142	eqtri	$$⊢1+1=02$$
231		1t1e1	$$⊢1\cdot 1=1$$
232		00id	$$⊢0+0=0$$
233	231 232	oveq12i	$$⊢1\cdot 1+0+0=1+0$$
234	233 79	eqtri	$$⊢1\cdot 1+0+0=1$$
235	231	oveq1i	$$⊢1\cdot 1+2=1+2$$
236		1p2e3	$$⊢1+2=3$$
237	235 236 193	3eqtri	$$⊢1\cdot 1+2=03$$
238	11 11 5 2 214 230 11 21 5 234 237	decmac	$$⊢11\cdot 1+1+1=13$$
239	93	mulridi	$$⊢6\cdot 1=6$$
240	239	oveq1i	$$⊢6\cdot 1+8=6+8$$
241	240 163	eqtri	$$⊢6\cdot 1+8=14$$
242	52 24 11 18 210 229 11 16 11 238 241	decmac	$$⊢116\cdot 1+18+0=134$$
243	231	oveq1i	$$⊢1\cdot 1+6=1+6$$
244	93 90 144	addcomli	$$⊢1+6=7$$
245	243 244 192	3eqtri	$$⊢1\cdot 1+6=07$$
246	61 11 63 24 70 227 11 30 5 242 245	decmac	$$⊢1161\cdot 1+70+116=1347$$
247	18	dec0h	$$⊢8=08$$
248	5	dec0h	$$⊢0=00$$
249	232 248	eqtri	$$⊢0+0=00$$
250	231	oveq1i	$$⊢1\cdot 1+0=1+0$$
251	250 79	eqtri	$$⊢1\cdot 1+0=1$$
252	11 11 5 5 214 249 11 251 251	decma	$$⊢11\cdot 1+0+0=11$$
253	239	oveq1i	$$⊢6\cdot 1+0=6+0$$
254	93	addridi	$$⊢6+0=6$$
255	253 254 87	3eqtri	$$⊢6\cdot 1+0=06$$
256	52 24 5 5 210 249 11 24 5 252 255	decmac	$$⊢116\cdot 1+0+0=116$$
257	231	oveq1i	$$⊢1\cdot 1+8=1+8$$
258	161 90 67	addcomli	$$⊢1+8=9$$
259	257 258 168	3eqtri	$$⊢1\cdot 1+8=09$$
260	61 11 5 18 70 247 11 27 5 256 259	decmac	$$⊢1161\cdot 1+8=1169$$
261	11 11 213 18 214 224 62 27 61 246 260	decma2c	$$⊢1161\cdot 11+11+697=13479$$
262	172 216	eqtri	$$⊢0+1=01$$
263	93	mullidi	$$⊢1\cdot 6=6$$
264	263 232	oveq12i	$$⊢1\cdot 6+0+0=6+0$$
265	264 254	eqtri	$$⊢1\cdot 6+0+0=6$$
266	263	oveq1i	$$⊢1\cdot 6+3=6+3$$
267	266 132 168	3eqtri	$$⊢1\cdot 6+3=09$$
268	11 11 5 21 214 194 24 27 5 265 267	decmac	$$⊢11\cdot 6+0+3=69$$
269		6t6e36	$$⊢6\cdot 6=36$$
270	21 24 144 269	decsuc	$$⊢6\cdot 6+1=37$$
271	52 24 5 11 210 262 24 30 21 268 270	decmac	$$⊢116\cdot 6+0+1=697$$
272	263	oveq1i	$$⊢1\cdot 6+6=6+6$$
273		6p6e12	$$⊢6+6=12$$
274	272 273	eqtri	$$⊢1\cdot 6+6=12$$
275	61 11 5 24 70 87 24 2 11 271 274	decmac	$$⊢1161\cdot 6+6=6972$$
276	52 24 52 24 210 210 62 2 212 261 275	decma2c	$$⊢1161\cdot 116+116=134792$$
277	62	nn0cni	$$⊢1161\in ℂ$$
278	277	mulridi	$$⊢1161\cdot 1=1161$$
279	62 61 11 70 11 61 276 278	decmul2c	$$⊢1161\cdot 1161=1347921$$
280	209 279	eqtr4i	$$⊢538\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1307=1161\cdot 1161$$
281	9 10 45 60 62 57 115 123 280	mod2xi	$$⊢2^{38}\mathrm{mod}N=1307\mathrm{mod}N$$
282		eqid	$$⊢38=38$$
283	21 18 67 282	decsuc	$$⊢38+1=39$$
284		eqid	$$⊢111=111$$
285	79 216	eqtri	$$⊢1+0=01$$
286	78 232	oveq12i	$$⊢1\cdot 2+0+0=2+0$$
287	77	addridi	$$⊢2+0=2$$
288	286 287	eqtri	$$⊢1\cdot 2+0+0=2$$
289	2 3 5 11 74 285 11 24 5 288 88	decma2c	$$⊢1\cdot 25+1+0=26$$
290	91	oveq1i	$$⊢1\cdot 0+1=0+1$$
291	290 172 216	3eqtri	$$⊢1\cdot 0+1=01$$
292	4 5 11 11 71 76 11 11 5 289 291	decma2c	$$⊢1\cdot 250+11+0=261$$
293	6 21 52 11 1 284 11 16 5 292 102	decma2c	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+111=2614$$
294	110	oveq1i	$$⊢3\cdot 2+0=6+0$$
295	294 254 87	3eqtri	$$⊢3\cdot 2+0=06$$
296	11 21 5 5 129 249 2 24 5 288 295	decmac	$$⊢13\cdot 2+0+0=26$$
297	77	mul02i	$$⊢0\cdot 2=0$$
298	297	oveq1i	$$⊢0\cdot 2+1=0+1$$
299	298 172 216	3eqtri	$$⊢0\cdot 2+1=01$$
300	55 5 5 11 127 216 2 11 5 296 299	decmac	$$⊢130\cdot 2+1=261$$
301		7t2e14	$$⊢7\cdot 2=14$$
302	2 56 30 124 16 11 300 301	decmul1c	$$⊢1307\cdot 2=2614$$
303	293 302	eqtr4i	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+111=1307\cdot 2$$
304	9 10 54 20 57 53 281 283 303	modxp1i	$$⊢2^{39}\mathrm{mod}N=111\mathrm{mod}N$$
305		eqid	$$⊢39=39$$
306	97 77 110	mulcomli	$$⊢2\cdot 3=6$$
307	306	oveq1i	$$⊢2\cdot 3+1=6+1$$
308	307 144	eqtri	$$⊢2\cdot 3+1=7$$
309	2 21 27 305 18 11 308 122	decmul2c	$$⊢2\cdot 39=78$$
310		eqid	$$⊢2309=2309$$
311		eqid	$$⊢230=230$$
312	34 5 2 311 135	decaddi	$$⊢230+2=232$$
313	34	nn0cni	$$⊢23\in ℂ$$
314	313	addridi	$$⊢23+0=23$$
315		4t2e8	$$⊢4\cdot 2=8$$
316		2p2e4	$$⊢2+2=4$$
317	315 316	oveq12i	$$⊢4\cdot 2+2+2=8+4$$
318		8p4e12	$$⊢8+4=12$$
319	317 318	eqtri	$$⊢4\cdot 2+2+2=12$$
320		5t4e20	$$⊢5\cdot 4=20$$
321	83 169 320	mulcomli	$$⊢4\cdot 5=20$$
322	2 5 21 321 157	decaddi	$$⊢4\cdot 5+3=23$$
323	2 3 2 21 74 314 16 21 2 319 322	decma2c	$$⊢4\cdot 25+23+0=123$$
324	169	mul01i	$$⊢4\cdot 0=0$$
325	324	oveq1i	$$⊢4\cdot 0+2=0+2$$
326	325 135 142	3eqtri	$$⊢4\cdot 0+2=02$$
327	4 5 34 2 71 312 16 2 5 323 326	decma2c	$$⊢4\cdot 250+230+2=1232$$
328		4t3e12	$$⊢4\cdot 3=12$$
329	11 2 27 328 131 11 149	decaddci	$$⊢4\cdot 3+9=21$$
330	6 21 48 27 1 310 16 11 2 327 329	decma2c	$$⊢4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2309=12321$$
331	5 11 11 11 216 214 172 131	decadd	$$⊢1+11=12$$
332	231	oveq1i	$$⊢1\cdot 1+1=1+1$$
333	332 131 142	3eqtri	$$⊢1\cdot 1+1=02$$
334	11 11 5 11 214 285 11 2 5 234 333	decmac	$$⊢11\cdot 1+1+0=12$$
335	52 11 11 2 284 331 11 21 5 334 237	decmac	$$⊢111\cdot 1+1+11=123$$
336	52 11 5 11 284 216 11 2 5 252 333	decmac	$$⊢111\cdot 1+1=112$$
337	11 11 11 11 214 214 53 2 52 335 336	decma2c	$$⊢111\cdot 11+11=1232$$
338	53	nn0cni	$$⊢111\in ℂ$$
339	338	mulridi	$$⊢111\cdot 1=111$$
340	53 52 11 284 11 52 337 339	decmul2c	$$⊢111\cdot 111=12321$$
341	330 340	eqtr4i	$$⊢4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2309=111\cdot 111$$
342	9 10 50 51 53 49 304 309 341	mod2xi	$$⊢2^{78}\mathrm{mod}N=2309\mathrm{mod}N$$
343		eqid	$$⊢78=78$$
344		4p1e5	$$⊢4+1=5$$
345	204 77 301	mulcomli	$$⊢2\cdot 7=14$$
346	11 16 344 345	decsuc	$$⊢2\cdot 7+1=15$$
347	161 77 108	mulcomli	$$⊢2\cdot 8=16$$
348	2 30 18 343 24 11 346 347	decmul2c	$$⊢2\cdot 78=156$$
349		eqid	$$⊢194=194$$
350	2 16	deccl	$$⊢24\in {\mathbb{N}}_0$$
351		eqid	$$⊢24=24$$
352	2 16 344 351	decsuc	$$⊢24+1=25$$
353		eqid	$$⊢23=23$$
354	2 21 100 353	decsuc	$$⊢23+1=24$$
355	34 5 11 27 311 116 354 183	decadd	$$⊢230+19=249$$
356	350 352 355	decsucc	$$⊢230+19+1=250$$
357		9p4e13	$$⊢9+4=13$$
358	48 27 45 16 310 349 356 21 357	decaddc	$$⊢2309+194=2503$$
359	358 1	eqtr4i	$$⊢2309+194=N$$
360		eqid	$$⊢91=91$$
361		eqid	$$⊢15=15$$
362	204	addlidi	$$⊢0+7=7$$
363	362 192	eqtri	$$⊢0+7=07$$
364	78 172	oveq12i	$$⊢1\cdot 2+0+1=2+1$$
365	364 81	eqtri	$$⊢1\cdot 2+0+1=3$$
366	11 5 30 156 362	decaddi	$$⊢5\cdot 2+7=17$$
367	11 3 5 30 361 363 2 30 11 365 366	decmac	$$⊢15\cdot 2+0+7=37$$
368	84 135	oveq12i	$$⊢1\cdot 5+0+2=5+2$$
369		5p2e7	$$⊢5+2=7$$
370	368 369	eqtri	$$⊢1\cdot 5+0+2=7$$
371	11 3 5 11 361 216 3 24 2 370 175	decmac	$$⊢15\cdot 5+1=76$$
372	2 3 5 11 74 285 39 24 30 367 371	decma2c	$$⊢15\cdot 25+1+0=376$$
373	39	nn0cni	$$⊢15\in ℂ$$
374	373	mul01i	$$⊢15\cdot 0=0$$
375	374	oveq1i	$$⊢15\cdot 0+3=0+3$$
376	375 157 193	3eqtri	$$⊢15\cdot 0+3=03$$
377	4 5 11 21 71 357 39 21 5 372 376	decma2c	$$⊢15\cdot 250+9+4=3763$$
378	98 172	oveq12i	$$⊢1\cdot 3+0+1=3+1$$
379	378 100	eqtri	$$⊢1\cdot 3+0+1=4$$
380	11 3 5 11 361 216 21 24 11 379 196	decmac	$$⊢15\cdot 3+1=46$$
381	6 21 27 11 1 360 39 24 16 377 380	decma2c	$$⊢15\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+91=37636$$
382	45 16	deccl	$$⊢194\in {\mathbb{N}}_0$$
383		eqid	$$⊢77=77$$
384	11 30	deccl	$$⊢17\in {\mathbb{N}}_0$$
385	384 3	deccl	$$⊢175\in {\mathbb{N}}_0$$
386		eqid	$$⊢175=175$$
387	384	nn0cni	$$⊢17\in ℂ$$
388	387	addlidi	$$⊢0+17=17$$
389	11 30 152 388	decsuc	$$⊢0+17+1=18$$
390		7p5e12	$$⊢7+5=12$$
391	5 30 384 3 192 386 389 2 390	decaddc	$$⊢7+175=182$$
392	231 131	oveq12i	$$⊢1\cdot 1+1+1=1+2$$
393	392 236	eqtri	$$⊢1\cdot 1+1+1=3$$
394	120	mulridi	$$⊢9\cdot 1=9$$
395	394	oveq1i	$$⊢9\cdot 1+8=9+8$$
396		9p8e17	$$⊢9+8=17$$
397	395 396	eqtri	$$⊢9\cdot 1+8=17$$
398	11 27 11 18 116 229 11 30 11 393 397	decmac	$$⊢19\cdot 1+18+0=37$$
399	169	mulridi	$$⊢4\cdot 1=4$$
400	399	oveq1i	$$⊢4\cdot 1+2=4+2$$
401		4p2e6	$$⊢4+2=6$$
402	400 401 87	3eqtri	$$⊢4\cdot 1+2=06$$
403	45 16 63 2 349 391 11 24 5 398 402	decmac	$$⊢194\cdot 1+7+175=376$$
404	120	mullidi	$$⊢1\cdot 9=9$$
405	161	addlidi	$$⊢0+8=8$$
406	404 405	oveq12i	$$⊢1\cdot 9+0+8=9+8$$
407	406 396	eqtri	$$⊢1\cdot 9+0+8=17$$
408		9t9e81	$$⊢9\cdot 9=81$$
409	169 90 344	addcomli	$$⊢1+4=5$$
410	18 11 16 408 409	decaddi	$$⊢9\cdot 9+4=85$$
411	11 27 5 16 116 171 27 3 18 407 410	decmac	$$⊢19\cdot 9+0+4=175$$
412		9t4e36	$$⊢9\cdot 4=36$$
413	120 169 412	mulcomli	$$⊢4\cdot 9=36$$
414		7p6e13	$$⊢7+6=13$$
415	204 93 414	addcomli	$$⊢6+7=13$$
416	21 24 30 413 100 21 415	decaddci	$$⊢4\cdot 9+7=43$$
417	45 16 5 30 349 192 27 21 16 411 416	decmac	$$⊢194\cdot 9+7=1753$$
418	11 27 30 30 116 383 382 21 385 403 417	decma2c	$$⊢194\cdot 19+77=3763$$
419	169	mullidi	$$⊢1\cdot 4=4$$
420	419 157	oveq12i	$$⊢1\cdot 4+0+3=4+3$$
421		4p3e7	$$⊢4+3=7$$
422	420 421	eqtri	$$⊢1\cdot 4+0+3=7$$
423	21 24 144 412	decsuc	$$⊢9\cdot 4+1=37$$
424	11 27 5 11 116 216 16 30 21 422 423	decmac	$$⊢19\cdot 4+1=77$$
425		4t4e16	$$⊢4\cdot 4=16$$
426	16 45 16 349 24 11 424 425	decmul1c	$$⊢194\cdot 4=776$$
427	382 45 16 349 24 37 418 426	decmul2c	$$⊢194\cdot 194=37636$$
428	381 427	eqtr4i	$$⊢15\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+91=194\cdot 194$$
429	10 43 44 47 42 49 342 348 359 428	mod2xnegi	$$⊢2^{156}\mathrm{mod}N=91\mathrm{mod}N$$
430		eqid	$$⊢156=156$$
431	117 172	oveq12i	$$⊢2\cdot 1+0+1=2+1$$
432	431 81	eqtri	$$⊢2\cdot 1+0+1=3$$
433	83 77 156	mulcomli	$$⊢2\cdot 5=10$$
434	11 5 172 433	decsuc	$$⊢2\cdot 5+1=11$$
435	11 3 5 11 361 216 2 11 11 432 434	decma2c	$$⊢2\cdot 15+1=31$$
436		6t2e12	$$⊢6\cdot 2=12$$
437	93 77 436	mulcomli	$$⊢2\cdot 6=12$$
438	2 39 24 430 2 11 435 437	decmul2c	$$⊢2\cdot 156=312$$
439		eqid	$$⊢772=772$$
440	30 30 152 383	decsuc	$$⊢77+1=78$$
441	204	addridi	$$⊢7+0=7$$
442	441 192	eqtri	$$⊢7+0=07$$
443	110 135	oveq12i	$$⊢3\cdot 2+0+2=6+2$$
444		6p2e8	$$⊢6+2=8$$
445	443 444	eqtri	$$⊢3\cdot 2+0+2=8$$
446	204 83 390	addcomli	$$⊢5+7=12$$
447	11 3 30 178 131 2 446	decaddci	$$⊢3\cdot 5+7=22$$
448	2 3 5 30 74 442 21 2 2 445 447	decma2c	$$⊢3\cdot 25+7+0=82$$
449	97	mul01i	$$⊢3\cdot 0=0$$
450	449	oveq1i	$$⊢3\cdot 0+8=0+8$$
451	450 405 247	3eqtri	$$⊢3\cdot 0+8=08$$
452	4 5 30 18 71 440 21 18 5 448 451	decma2c	$$⊢3\cdot 250+77+1=828$$
453	198	oveq1i	$$⊢3\cdot 3+2=9+2$$
454	453 148	eqtri	$$⊢3\cdot 3+2=11$$
455	6 21 37 2 1 439 21 11 11 452 454	decma2c	$$⊢3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+772=8281$$
456	18 11 131 408	decsuc	$$⊢9\cdot 9+1=82$$
457	404	oveq1i	$$⊢1\cdot 9+9=9+9$$
458		9p9e18	$$⊢9+9=18$$
459	457 458	eqtri	$$⊢1\cdot 9+9=18$$
460	27 11 27 360 27 18 11 456 459	decrmac	$$⊢91\cdot 9+9=828$$
461	42	nn0cni	$$⊢91\in ℂ$$
462	461	mulridi	$$⊢91\cdot 1=91$$
463	42 27 11 360 11 27 460 462	decmul2c	$$⊢91\cdot 91=8281$$
464	455 463	eqtr4i	$$⊢3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+772=91\cdot 91$$
465	9 10 40 41 42 38 429 438 464	mod2xi	$$⊢2^{312}\mathrm{mod}N=772\mathrm{mod}N$$
466		eqid	$$⊢312=312$$
467		eqid	$$⊢31=31$$
468	306	oveq1i	$$⊢2\cdot 3+0=6+0$$
469	468 254	eqtri	$$⊢2\cdot 3+0=6$$
470	117 142	eqtri	$$⊢2\cdot 1=02$$
471	2 21 11 467 2 5 469 470	decmul2c	$$⊢2\cdot 31=62$$
472	471	oveq1i	$$⊢2\cdot 31+0=62+0$$
473	25	nn0cni	$$⊢62\in ℂ$$
474	473	addridi	$$⊢62+0=62$$
475	472 474	eqtri	$$⊢2\cdot 31+0=62$$
476	112 101	eqtri	$$⊢2\cdot 2=04$$
477	2 22 2 466 16 5 475 476	decmul2c	$$⊢2\cdot 312=624$$
478		eqid	$$⊢270=270$$
479	30 11	deccl	$$⊢71\in {\mathbb{N}}_0$$
480		eqid	$$⊢71=71$$
481		7p2e9	$$⊢7+2=9$$
482	204 77 481	addcomli	$$⊢2+7=9$$
483	2 30 30 11 153 480 482 152	decadd	$$⊢27+71=98$$
484	120	addridi	$$⊢9+0=9$$
485	484 168	eqtri	$$⊢9+0=09$$
486	52 27	deccl	$$⊢119\in {\mathbb{N}}_0$$
487		eqid	$$⊢238=238$$
488	486	nn0cni	$$⊢119\in ℂ$$
489	488	addlidi	$$⊢0+119=119$$
490	11 11 2 214 236	decaddi	$$⊢11+2=13$$
491	112 79	oveq12i	$$⊢2\cdot 2+1+0=4+1$$
492	491 344	eqtri	$$⊢2\cdot 2+1+0=5$$
493	110	oveq1i	$$⊢3\cdot 2+3=6+3$$
494	493 132 168	3eqtri	$$⊢3\cdot 2+3=09$$
495	2 21 11 21 353 490 2 27 5 492 494	decmac	$$⊢23\cdot 2+11+2=59$$
496		9p6e15	$$⊢9+6=15$$
497	120 93 496	addcomli	$$⊢6+9=15$$
498	11 24 27 108 131 3 497	decaddci	$$⊢8\cdot 2+9=25$$
499	34 18 52 27 487 489 2 3 2 495 498	decmac	$$⊢238\cdot 2+0+119=595$$
500	172	oveq2i	$$⊢2\cdot 5+0+1=2\cdot 5+1$$
501	500 434	eqtri	$$⊢2\cdot 5+0+1=11$$
502	2 21 5 16 353 171 3 27 11 501 180	decmac	$$⊢23\cdot 5+0+4=119$$
503	34 18 5 27 487 168 3 27 16 502 184	decmac	$$⊢238\cdot 5+9=1199$$
504	2 3 5 27 74 485 35 27 486 499 503	decma2c	$$⊢238\cdot 25+9+0=5959$$
505	35	nn0cni	$$⊢238\in ℂ$$
506	505	mul01i	$$⊢238\cdot 0=0$$
507	506	oveq1i	$$⊢238\cdot 0+8=0+8$$
508	507 405 247	3eqtri	$$⊢238\cdot 0+8=08$$
509	4 5 27 18 71 483 35 18 5 504 508	decma2c	$$⊢238\cdot 250+27+71=59598$$
510	306 172	oveq12i	$$⊢2\cdot 3+0+1=6+1$$
511	510 144	eqtri	$$⊢2\cdot 3+0+1=7$$
512	2 21 5 2 353 142 21 11 11 511 454	decmac	$$⊢23\cdot 3+2=71$$
513	21 34 18 487 16 2 512 203	decmul1c	$$⊢238\cdot 3=714$$
514	513	oveq1i	$$⊢238\cdot 3+0=714+0$$
515	479 16	deccl	$$⊢714\in {\mathbb{N}}_0$$
516	515	nn0cni	$$⊢714\in ℂ$$
517	516	addridi	$$⊢714+0=714$$
518	514 517	eqtri	$$⊢238\cdot 3+0=714$$
519	6 21 31 5 1 478 35 16 479 509 518	decma2c	$$⊢238\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+270=595984$$
520	39 16	deccl	$$⊢154\in {\mathbb{N}}_0$$
521		eqid	$$⊢154=154$$
522	3 16	deccl	$$⊢54\in {\mathbb{N}}_0$$
523	522 5	deccl	$$⊢540\in {\mathbb{N}}_0$$
524	3 3	deccl	$$⊢55\in {\mathbb{N}}_0$$
525		eqid	$$⊢540=540$$
526		eqid	$$⊢54=54$$
527	83	addlidi	$$⊢0+5=5$$
528	5 11 3 16 216 526 527 409	decadd	$$⊢1+54=55$$
529	83	addridi	$$⊢5+0=5$$
530	11 3 522 5 361 525 528 529	decadd	$$⊢15+540=555$$
531		eqid	$$⊢55=55$$
532	3 3 86 531	decsuc	$$⊢55+1=56$$
533		7t7e49	$$⊢7\cdot 7=49$$
534		5p5e10	$$⊢5+5=10$$
535	16 27 11 5 533 534 344 484	decadd	$$⊢7\cdot 7+5+5=59$$
536	16 27 24 533 344 3 496	decaddci	$$⊢7\cdot 7+6=55$$
537	30 30 3 24 383 532 30 3 3 535 536	decmac	$$⊢77\cdot 7+55+1=595$$
538	83 169 179	addcomli	$$⊢4+5=9$$
539	11 16 3 345 538	decaddi	$$⊢2\cdot 7+5=19$$
540	37 2 524 3 439 530 30 27 11 537 539	decmac	$$⊢772\cdot 7+15+540=5959$$
541	527	oveq2i	$$⊢7\cdot 7+0+5=7\cdot 7+5$$
542		9p5e14	$$⊢9+5=14$$
543	16 27 3 533 344 16 542	decaddci	$$⊢7\cdot 7+5=54$$
544	541 543	eqtri	$$⊢7\cdot 7+0+5=54$$
545	16 344 533	decsucc	$$⊢7\cdot 7+1=50$$
546	30 30 5 11 383 262 30 5 3 544 545	decmac	$$⊢77\cdot 7+0+1=540$$
547		4p4e8	$$⊢4+4=8$$
548	11 16 16 345 547	decaddi	$$⊢2\cdot 7+4=18$$
549	37 2 5 16 439 101 30 18 11 546 548	decmac	$$⊢772\cdot 7+4=5408$$
550	30 30 39 16 383 521 38 18 523 540 549	decma2c	$$⊢772\cdot 77+154=59598$$
551	11 16 344 301	decsuc	$$⊢7\cdot 2+1=15$$
552	2 30 30 383 16 11 551 301	decmul1c	$$⊢77\cdot 2=154$$
553	2 37 2 439 552 112	decmul1	$$⊢772\cdot 2=1544$$
554	38 37 2 439 16 520 550 553	decmul2c	$$⊢772\cdot 772=595984$$
555	519 554	eqtr4i	$$⊢238\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+270=772\cdot 772$$
556	9 10 33 36 38 32 465 477 555	mod2xi	$$⊢2^{624}\mathrm{mod}N=270\mathrm{mod}N$$
557		eqid	$$⊢624=624$$
558		eqid	$$⊢62=62$$
559	437	oveq1i	$$⊢2\cdot 6+0=12+0$$
560	12	nn0cni	$$⊢12\in ℂ$$
561	560	addridi	$$⊢12+0=12$$
562	559 561	eqtri	$$⊢2\cdot 6+0=12$$
563	2 24 2 558 16 5 562 476	decmul2c	$$⊢2\cdot 62=124$$
564	563	oveq1i	$$⊢2\cdot 62+0=124+0$$
565	17	nn0cni	$$⊢124\in ℂ$$
566	565	addridi	$$⊢124+0=124$$
567	564 566	eqtri	$$⊢2\cdot 62+0=124$$
568	169 77 315	mulcomli	$$⊢2\cdot 4=8$$
569	568 247	eqtri	$$⊢2\cdot 4=08$$
570	2 25 16 557 18 5 567 569	decmul2c	$$⊢2\cdot 624=1248$$
571		eqid	$$⊢313=313$$
572	21 11 27 467 100 221	decaddci2	$$⊢31+9=40$$
573	169	addridi	$$⊢4+0=4$$
574	573 101	eqtri	$$⊢4+0=04$$
575	11 16	deccl	$$⊢14\in {\mathbb{N}}_0$$
576		eqid	$$⊢29=29$$
577	575	nn0cni	$$⊢14\in ℂ$$
578	577	addlidi	$$⊢0+14=14$$
579	112 236	oveq12i	$$⊢2\cdot 2+1+2=4+3$$
580	579 421	eqtri	$$⊢2\cdot 2+1+2=7$$
581	11 18 16 121 131 2 318	decaddci	$$⊢9\cdot 2+4=22$$
582	2 27 11 16 576 578 2 2 2 580 581	decmac	$$⊢29\cdot 2+0+14=72$$
583	11 5 16 433 170	decaddi	$$⊢2\cdot 5+4=14$$
584		9t5e45	$$⊢9\cdot 5=45$$
585	16 3 16 584 179	decaddi	$$⊢9\cdot 5+4=49$$
586	2 27 16 576 3 27 16 583 585	decrmac	$$⊢29\cdot 5+4=149$$
587	2 3 5 16 74 574 28 27 575 582 586	decma2c	$$⊢29\cdot 25+4+0=729$$
588	137	mul01i	$$⊢29\cdot 0=0$$
589	588	oveq1i	$$⊢29\cdot 0+0=0+0$$
590	589 232 248	3eqtri	$$⊢29\cdot 0+0=00$$
591	4 5 16 5 71 572 28 5 5 587 590	decma2c	$$⊢29\cdot 250+31+9=7290$$
592	306 157	oveq12i	$$⊢2\cdot 3+0+3=6+3$$
593	592 132	eqtri	$$⊢2\cdot 3+0+3=9$$
594		9t3e27	$$⊢9\cdot 3=27$$
595		7p3e10	$$⊢7+3=10$$
596	2 30 21 594 81 595	decaddci2	$$⊢9\cdot 3+3=30$$
597	2 27 5 21 576 193 21 5 21 593 596	decmac	$$⊢29\cdot 3+3=90$$
598	6 21 22 21 1 571 28 5 27 591 597	decma2c	$$⊢29\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+313=72900$$
599	63 27	deccl	$$⊢189\in {\mathbb{N}}_0$$
600		eqid	$$⊢189=189$$
601	161 169 318	addcomli	$$⊢4+8=12$$
602	11 16 18 301 131 2 601	decaddci	$$⊢7\cdot 2+8=22$$
603	2 30 11 18 153 229 2 2 2 580 602	decmac	$$⊢27\cdot 2+18+0=72$$
604	297	oveq1i	$$⊢0\cdot 2+9=0+9$$
605	604 183 168	3eqtri	$$⊢0\cdot 2+9=09$$
606	31 5 63 27 478 600 2 27 5 603 605	decmac	$$⊢270\cdot 2+189=729$$
607	30 2 30 153 27 16 548 533	decmul1c	$$⊢27\cdot 7=189$$
608	204	mul02i	$$⊢0\cdot 7=0$$
609	30 31 5 478 607 608	decmul1	$$⊢270\cdot 7=1890$$
610	32 2 30 153 5 599 606 609	decmul2c	$$⊢270\cdot 27=7290$$
611	610	oveq1i	$$⊢270\cdot 27+0=7290+0$$
612	30 2	deccl	$$⊢72\in {\mathbb{N}}_0$$
613	612 27	deccl	$$⊢729\in {\mathbb{N}}_0$$
614	613 5	deccl	$$⊢7290\in {\mathbb{N}}_0$$
615	614	nn0cni	$$⊢7290\in ℂ$$
616	615	addridi	$$⊢7290+0=7290$$
617	611 616	eqtri	$$⊢270\cdot 27+0=7290$$
618	32	nn0cni	$$⊢270\in ℂ$$
619	618	mul01i	$$⊢270\cdot 0=0$$
620	619 248	eqtri	$$⊢270\cdot 0=00$$
621	32 31 5 478 5 5 617 620	decmul2c	$$⊢270\cdot 270=72900$$
622	598 621	eqtr4i	$$⊢29\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+313=270\cdot 270$$
623	9 10 26 29 32 23 556 570 622	mod2xi	$$⊢2^{1248}\mathrm{mod}N=313\mathrm{mod}N$$
624		cu2	$$⊢2^3=8$$
625	624	oveq1i	$$⊢2^3\mathrm{mod}N=8\mathrm{mod}N$$
626		eqid	$$⊢1248=1248$$
627		eqid	$$⊢124=124$$
628	12 16 344 627	decsuc	$$⊢124+1=125$$
629		8p3e11	$$⊢8+3=11$$
630	17 18 21 626 628 11 629	decaddci	$$⊢1248+3=1251$$
631	9	nncni	$$⊢N\in ℂ$$
632	631	mullidi	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
633	632 1	eqtri	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=2503$$
634	6 21 100 633	decsuc	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=2504$$
635	161 97 203	mulcomli	$$⊢3\cdot 8=24$$
636	2 16 344 635	decsuc	$$⊢3\cdot 8+1=25$$
637	161	mullidi	$$⊢1\cdot 8=8$$
638	637	oveq1i	$$⊢1\cdot 8+2=8+2$$
639		8p2e10	$$⊢8+2=10$$
640	638 639	eqtri	$$⊢1\cdot 8+2=10$$
641	21 11 2 467 18 5 11 636 640	decrmac	$$⊢31\cdot 8+2=250$$
642	18 22 21 571 16 2 641 635	decmul1c	$$⊢313\cdot 8=2504$$
643	634 642	eqtr4i	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=313\cdot 8$$
644	9 10 19 20 23 11 21 18 623 625 630 643	modxai	$$⊢2^{1251}\mathrm{mod}N=1\mathrm{mod}N$$
645		eqid	$$⊢1251=1251$$
646		eqid	$$⊢125=125$$
647		eqid	$$⊢12=12$$
648	117 232	oveq12i	$$⊢2\cdot 1+0+0=2+0$$
649	648 287	eqtri	$$⊢2\cdot 1+0+0=2$$
650	112	oveq1i	$$⊢2\cdot 2+1=4+1$$
651	3	dec0h	$$⊢5=05$$
652	650 344 651	3eqtri	$$⊢2\cdot 2+1=05$$
653	11 2 5 11 647 216 2 3 5 649 652	decma2c	$$⊢2\cdot 12+1=25$$
654	2 12 3 646 5 11 653 433	decmul2c	$$⊢2\cdot 125=250$$
655	4 5 5 654 232	decaddi	$$⊢2\cdot 125+0=250$$
656	2 13 11 645 2 5 655 470	decmul2c	$$⊢2\cdot 1251=2502$$
657	6 2	deccl	$$⊢2502\in {\mathbb{N}}_0$$
658	657	nn0cni	$$⊢2502\in ℂ$$
659		eqid	$$⊢2502=2502$$
660	6 2 81 659	decsuc	$$⊢2502+1=2503$$
661	1 660	eqtr4i	$$⊢N=2502+1$$
662	658 90 661	mvrraddi	$$⊢N-1=2502$$
663	656 662	eqtr4i	$$⊢2\cdot 1251=N-1$$
664	631	mul02i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0$$
665	664	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=0+1$$
666	231 172	eqtr4i	$$⊢1\cdot 1=0+1$$
667	665 666	eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=1\cdot 1$$
668	9 10 14 15 11 11 644 663 667	mod2xi	$$⊢2^{N-1}\mathrm{mod}N=1\mathrm{mod}N$$