Theorem 1259lem4

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

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

Proof

Step	Hyp	Ref	Expression
1		1259prm.1	$$⊢N=1259$$
2		2nn	$$⊢2\in \mathbb{N}$$
3		6nn0	$$⊢6\in {\mathbb{N}}_0$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢62\in {\mathbb{N}}_0$$
6		9nn0	$$⊢9\in {\mathbb{N}}_0$$
7	5 6	deccl	$$⊢629\in {\mathbb{N}}_0$$
8		0z	$$⊢0\in \mathbb{Z}$$
9		1nn	$$⊢1\in \mathbb{N}$$
10		1nn0	$$⊢1\in {\mathbb{N}}_0$$
11	10 4	deccl	$$⊢12\in {\mathbb{N}}_0$$
12		5nn0	$$⊢5\in {\mathbb{N}}_0$$
13	11 12	deccl	$$⊢125\in {\mathbb{N}}_0$$
14		8nn0	$$⊢8\in {\mathbb{N}}_0$$
15	13 14	deccl	$$⊢1258\in {\mathbb{N}}_0$$
16	15	nn0cni	$$⊢1258\in ℂ$$
17		ax-1cn	$$⊢1\in ℂ$$
18		8p1e9	$$⊢8+1=9$$
19		eqid	$$⊢1258=1258$$
20	13 14 18 19	decsuc	$$⊢1258+1=1259$$
21	1 20	eqtr4i	$$⊢N=1258+1$$
22	16 17 21	mvrraddi	$$⊢N-1=1258$$
23	22 15	eqeltri	$$⊢N-1\in {\mathbb{N}}_0$$
24		9nn	$$⊢9\in \mathbb{N}$$
25	13 24	decnncl	$$⊢1259\in \mathbb{N}$$
26	1 25	eqeltri	$$⊢N\in \mathbb{N}$$
27	3 10	deccl	$$⊢61\in {\mathbb{N}}_0$$
28	27 4	deccl	$$⊢612\in {\mathbb{N}}_0$$
29		3nn0	$$⊢3\in {\mathbb{N}}_0$$
30		4nn0	$$⊢4\in {\mathbb{N}}_0$$
31	29 30	deccl	$$⊢34\in {\mathbb{N}}_0$$
32	31	nn0zi	$$⊢34\in \mathbb{Z}$$
33	29 4	deccl	$$⊢32\in {\mathbb{N}}_0$$
34	33 30	deccl	$$⊢324\in {\mathbb{N}}_0$$
35		7nn0	$$⊢7\in {\mathbb{N}}_0$$
36	10 35	deccl	$$⊢17\in {\mathbb{N}}_0$$
37	10 29	deccl	$$⊢13\in {\mathbb{N}}_0$$
38	37 3	deccl	$$⊢136\in {\mathbb{N}}_0$$
39		0nn0	$$⊢0\in {\mathbb{N}}_0$$
40	29 39	deccl	$$⊢30\in {\mathbb{N}}_0$$
41	40 3	deccl	$$⊢306\in {\mathbb{N}}_0$$
42		8nn	$$⊢8\in \mathbb{N}$$
43	10 42	decnncl	$$⊢18\in \mathbb{N}$$
44	11 30	deccl	$$⊢124\in {\mathbb{N}}_0$$
45	44 10	deccl	$$⊢1241\in {\mathbb{N}}_0$$
46	10 12	deccl	$$⊢15\in {\mathbb{N}}_0$$
47	46 29	deccl	$$⊢153\in {\mathbb{N}}_0$$
48		1z	$$⊢1\in \mathbb{Z}$$
49	12 39	deccl	$$⊢50\in {\mathbb{N}}_0$$
50	46 4	deccl	$$⊢152\in {\mathbb{N}}_0$$
51	4 12	deccl	$$⊢25\in {\mathbb{N}}_0$$
52	35 3	deccl	$$⊢76\in {\mathbb{N}}_0$$
53	1	1259lem3	$$⊢2^{76}\mathrm{mod}N=5\mathrm{mod}N$$
54		eqid	$$⊢76=76$$
55		4p1e5	$$⊢4+1=5$$
56		7cn	$$⊢7\in ℂ$$
57		2cn	$$⊢2\in ℂ$$
58		7t2e14	$$⊢7\cdot 2=14$$
59	56 57 58	mulcomli	$$⊢2\cdot 7=14$$
60	10 30 55 59	decsuc	$$⊢2\cdot 7+1=15$$
61		6cn	$$⊢6\in ℂ$$
62		6t2e12	$$⊢6\cdot 2=12$$
63	61 57 62	mulcomli	$$⊢2\cdot 6=12$$
64	4 35 3 54 4 10 60 63	decmul2c	$$⊢2\cdot 76=152$$
65	51	nn0cni	$$⊢25\in ℂ$$
66	65	addlidi	$$⊢0+25=25$$
67	26	nncni	$$⊢N\in ℂ$$
68	67	mul02i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0$$
69	68	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+25=0+25$$
70		5t5e25	$$⊢5\cdot 5=25$$
71	66 69 70	3eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+25=5\cdot 5$$
72	26 2 52 8 12 51 53 64 71	mod2xi	$$⊢2^{152}\mathrm{mod}N=25\mathrm{mod}N$$
73		2p1e3	$$⊢2+1=3$$
74		eqid	$$⊢152=152$$
75	46 4 73 74	decsuc	$$⊢152+1=153$$
76	49	nn0cni	$$⊢50\in ℂ$$
77	76	addlidi	$$⊢0+50=50$$
78	68	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+50=0+50$$
79		eqid	$$⊢25=25$$
80		2t2e4	$$⊢2\cdot 2=4$$
81	80	oveq1i	$$⊢2\cdot 2+1=4+1$$
82	81 55	eqtri	$$⊢2\cdot 2+1=5$$
83		5t2e10	$$⊢5\cdot 2=10$$
84	4 4 12 79 39 10 82 83	decmul1c	$$⊢25\cdot 2=50$$
85	77 78 84	3eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+50=25\cdot 2$$
86	26 2 50 8 51 49 72 75 85	modxp1i	$$⊢2^{153}\mathrm{mod}N=50\mathrm{mod}N$$
87		eqid	$$⊢153=153$$
88		eqid	$$⊢15=15$$
89	57	mulridi	$$⊢2\cdot 1=2$$
90	89	oveq1i	$$⊢2\cdot 1+1=2+1$$
91	90 73	eqtri	$$⊢2\cdot 1+1=3$$
92		5cn	$$⊢5\in ℂ$$
93	92 57 83	mulcomli	$$⊢2\cdot 5=10$$
94	4 10 12 88 39 10 91 93	decmul2c	$$⊢2\cdot 15=30$$
95	94	oveq1i	$$⊢2\cdot 15+0=30+0$$
96	40	nn0cni	$$⊢30\in ℂ$$
97	96	addridi	$$⊢30+0=30$$
98	95 97	eqtri	$$⊢2\cdot 15+0=30$$
99		2t3e6	$$⊢2\cdot 3=6$$
100	3	dec0h	$$⊢6=06$$
101	99 100	eqtri	$$⊢2\cdot 3=06$$
102	4 46 29 87 3 39 98 101	decmul2c	$$⊢2\cdot 153=306$$
103	67	mullidi	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
104	103 1	eqtri	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=1259$$
105		eqid	$$⊢1241=1241$$
106	4 30	deccl	$$⊢24\in {\mathbb{N}}_0$$
107		eqid	$$⊢24=24$$
108	4 30 55 107	decsuc	$$⊢24+1=25$$
109		eqid	$$⊢125=125$$
110		eqid	$$⊢124=124$$
111		eqid	$$⊢12=12$$
112		1p1e2	$$⊢1+1=2$$
113		2p2e4	$$⊢2+2=4$$
114	10 4 10 4 111 111 112 113	decadd	$$⊢12+12=24$$
115		5p4e9	$$⊢5+4=9$$
116	11 12 11 30 109 110 114 115	decadd	$$⊢125+124=249$$
117	106 108 116	decsucc	$$⊢125+124+1=250$$
118		9p1e10	$$⊢9+1=10$$
119	13 6 44 10 104 105 117 118	decaddc2	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1241=2500$$
120		eqid	$$⊢50=50$$
121	92	mul02i	$$⊢0\cdot 5=0$$
122	12 12 39 120 70 121	decmul1	$$⊢50\cdot 5=250$$
123	122	oveq1i	$$⊢50\cdot 5+0=250+0$$
124	51 39	deccl	$$⊢250\in {\mathbb{N}}_0$$
125	124	nn0cni	$$⊢250\in ℂ$$
126	125	addridi	$$⊢250+0=250$$
127	123 126	eqtri	$$⊢50\cdot 5+0=250$$
128	76	mul01i	$$⊢50\cdot 0=0$$
129	39	dec0h	$$⊢0=00$$
130	128 129	eqtri	$$⊢50\cdot 0=00$$
131	49 12 39 120 39 39 127 130	decmul2c	$$⊢50\cdot 50=2500$$
132	119 131	eqtr4i	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1241=50\cdot 50$$
133	26 2 47 48 49 45 86 102 132	mod2xi	$$⊢2^{306}\mathrm{mod}N=1241\mathrm{mod}N$$
134		eqid	$$⊢306=306$$
135		eqid	$$⊢30=30$$
136	10	dec0h	$$⊢1=01$$
137		00id	$$⊢0+0=0$$
138	99 137	oveq12i	$$⊢2\cdot 3+0+0=6+0$$
139	61	addridi	$$⊢6+0=6$$
140	138 139	eqtri	$$⊢2\cdot 3+0+0=6$$
141	57	mul01i	$$⊢2\cdot 0=0$$
142	141	oveq1i	$$⊢2\cdot 0+1=0+1$$
143		0p1e1	$$⊢0+1=1$$
144	142 143 136	3eqtri	$$⊢2\cdot 0+1=01$$
145	29 39 39 10 135 136 4 10 39 140 144	decma2c	$$⊢2\cdot 30+1=61$$
146	4 40 3 134 4 10 145 63	decmul2c	$$⊢2\cdot 306=612$$
147		eqid	$$⊢18=18$$
148	11 30 55 110	decsuc	$$⊢124+1=125$$
149		8cn	$$⊢8\in ℂ$$
150	149 17 18	addcomli	$$⊢1+8=9$$
151	44 10 10 14 105 147 148 150	decadd	$$⊢1241+18=1259$$
152	151 1	eqtr4i	$$⊢1241+18=N$$
153	34	nn0cni	$$⊢324\in ℂ$$
154	153	addlidi	$$⊢0+324=324$$
155	68	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+324=0+324$$
156	10 14	deccl	$$⊢18\in {\mathbb{N}}_0$$
157	10 30	deccl	$$⊢14\in {\mathbb{N}}_0$$
158		eqid	$$⊢14=14$$
159	17	mulridi	$$⊢1\cdot 1=1$$
160	159 112	oveq12i	$$⊢1\cdot 1+1+1=1+2$$
161		1p2e3	$$⊢1+2=3$$
162	160 161	eqtri	$$⊢1\cdot 1+1+1=3$$
163	149	mulridi	$$⊢8\cdot 1=8$$
164	163	oveq1i	$$⊢8\cdot 1+4=8+4$$
165		8p4e12	$$⊢8+4=12$$
166	164 165	eqtri	$$⊢8\cdot 1+4=12$$
167	10 14 10 30 147 158 10 4 10 162 166	decmac	$$⊢18\cdot 1+14=32$$
168	149	mullidi	$$⊢1\cdot 8=8$$
169	168	oveq1i	$$⊢1\cdot 8+6=8+6$$
170		8p6e14	$$⊢8+6=14$$
171	169 170	eqtri	$$⊢1\cdot 8+6=14$$
172		8t8e64	$$⊢8\cdot 8=64$$
173	14 10 14 147 30 3 171 172	decmul1c	$$⊢18\cdot 8=144$$
174	156 10 14 147 30 157 167 173	decmul2c	$$⊢18\cdot 18=324$$
175	154 155 174	3eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+324=18\cdot 18$$
176	2 41 8 43 34 45 133 146 152 175	mod2xnegi	$$⊢2^{612}\mathrm{mod}N=324\mathrm{mod}N$$
177	1	1259lem1	$$⊢2^{17}\mathrm{mod}N=136\mathrm{mod}N$$
178		eqid	$$⊢612=612$$
179		eqid	$$⊢17=17$$
180		eqid	$$⊢61=61$$
181	3 10 112 180	decsuc	$$⊢61+1=62$$
182		7p2e9	$$⊢7+2=9$$
183	56 57 182	addcomli	$$⊢2+7=9$$
184	27 4 10 35 178 179 181 183	decadd	$$⊢612+17=629$$
185	29 10	deccl	$$⊢31\in {\mathbb{N}}_0$$
186		eqid	$$⊢31=31$$
187		3cn	$$⊢3\in ℂ$$
188		3p2e5	$$⊢3+2=5$$
189	187 57 188	addcomli	$$⊢2+3=5$$
190	10 4 29 111 189	decaddi	$$⊢12+3=15$$
191		5p1e6	$$⊢5+1=6$$
192	11 12 29 10 109 186 190 191	decadd	$$⊢125+31=156$$
193	112	oveq1i	$$⊢1+1+1=2+1$$
194	193 73	eqtri	$$⊢1+1+1=3$$
195		7p5e12	$$⊢7+5=12$$
196	56 92 195	addcomli	$$⊢5+7=12$$
197	10 12 10 35 88 179 194 4 196	decaddc	$$⊢15+17=32$$
198		eqid	$$⊢34=34$$
199		7p3e10	$$⊢7+3=10$$
200	56 187 199	addcomli	$$⊢3+7=10$$
201	187	mulridi	$$⊢3\cdot 1=3$$
202	17	addridi	$$⊢1+0=1$$
203	201 202	oveq12i	$$⊢3\cdot 1+1+0=3+1$$
204		3p1e4	$$⊢3+1=4$$
205	203 204	eqtri	$$⊢3\cdot 1+1+0=4$$
206		4cn	$$⊢4\in ℂ$$
207	206	mulridi	$$⊢4\cdot 1=4$$
208	207	oveq1i	$$⊢4\cdot 1+0=4+0$$
209	206	addridi	$$⊢4+0=4$$
210	30	dec0h	$$⊢4=04$$
211	208 209 210	3eqtri	$$⊢4\cdot 1+0=04$$
212	29 30 10 39 198 200 10 30 39 205 211	decmac	$$⊢34\cdot 1+3+7=44$$
213	4	dec0h	$$⊢2=02$$
214		3t2e6	$$⊢3\cdot 2=6$$
215	214 143	oveq12i	$$⊢3\cdot 2+0+1=6+1$$
216		6p1e7	$$⊢6+1=7$$
217	215 216	eqtri	$$⊢3\cdot 2+0+1=7$$
218		4t2e8	$$⊢4\cdot 2=8$$
219	218	oveq1i	$$⊢4\cdot 2+2=8+2$$
220		8p2e10	$$⊢8+2=10$$
221	219 220	eqtri	$$⊢4\cdot 2+2=10$$
222	29 30 39 4 198 213 4 39 10 217 221	decmac	$$⊢34\cdot 2+2=70$$
223	10 4 29 4 111 197 31 39 35 212 222	decma2c	$$⊢34\cdot 12+15+17=440$$
224		5t3e15	$$⊢5\cdot 3=15$$
225	92 187 224	mulcomli	$$⊢3\cdot 5=15$$
226		5p2e7	$$⊢5+2=7$$
227	10 12 4 225 226	decaddi	$$⊢3\cdot 5+2=17$$
228		5t4e20	$$⊢5\cdot 4=20$$
229	92 206 228	mulcomli	$$⊢4\cdot 5=20$$
230	61	addlidi	$$⊢0+6=6$$
231	4 39 3 229 230	decaddi	$$⊢4\cdot 5+6=26$$
232	29 30 3 198 12 3 4 227 231	decrmac	$$⊢34\cdot 5+6=176$$
233	11 12 46 3 109 192 31 3 36 223 232	decma2c	$$⊢34\cdot 125+125+31=4406$$
234		9cn	$$⊢9\in ℂ$$
235		9t3e27	$$⊢9\cdot 3=27$$
236	234 187 235	mulcomli	$$⊢3\cdot 9=27$$
237		7p4e11	$$⊢7+4=11$$
238	4 35 30 236 73 10 237	decaddci	$$⊢3\cdot 9+4=31$$
239		9t4e36	$$⊢9\cdot 4=36$$
240	234 206 239	mulcomli	$$⊢4\cdot 9=36$$
241	149 61 170	addcomli	$$⊢6+8=14$$
242	29 3 14 240 204 30 241	decaddci	$$⊢4\cdot 9+8=44$$
243	29 30 14 198 6 30 30 238 242	decrmac	$$⊢34\cdot 9+8=314$$
244	13 6 13 14 1 22 31 30 185 233 243	decma2c	$$⊢34\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+N-1=44064$$
245		eqid	$$⊢136=136$$
246	10 6	deccl	$$⊢19\in {\mathbb{N}}_0$$
247	246 30	deccl	$$⊢194\in {\mathbb{N}}_0$$
248		eqid	$$⊢13=13$$
249		eqid	$$⊢194=194$$
250	6 35	deccl	$$⊢97\in {\mathbb{N}}_0$$
251	10 10	deccl	$$⊢11\in {\mathbb{N}}_0$$
252		eqid	$$⊢324=324$$
253		eqid	$$⊢19=19$$
254		eqid	$$⊢97=97$$
255	234 17 118	addcomli	$$⊢1+9=10$$
256	10 39 143 255	decsuc	$$⊢1+9+1=11$$
257		9p7e16	$$⊢9+7=16$$
258	10 6 6 35 253 254 256 3 257	decaddc	$$⊢19+97=116$$
259		eqid	$$⊢32=32$$
260		eqid	$$⊢11=11$$
261	10 10 112 260	decsuc	$$⊢11+1=12$$
262	89	oveq1i	$$⊢2\cdot 1+2=2+2$$
263	262 113 210	3eqtri	$$⊢2\cdot 1+2=04$$
264	29 4 10 4 259 261 10 30 39 205 263	decmac	$$⊢32\cdot 1+11+1=44$$
265	207	oveq1i	$$⊢4\cdot 1+6=4+6$$
266		6p4e10	$$⊢6+4=10$$
267	61 206 266	addcomli	$$⊢4+6=10$$
268	265 267	eqtri	$$⊢4\cdot 1+6=10$$
269	33 30 251 3 252 258 10 39 10 264 268	decmac	$$⊢324\cdot 1+19+97=440$$
270	143 136	eqtri	$$⊢0+1=01$$
271		3t3e9	$$⊢3\cdot 3=9$$
272	271 137	oveq12i	$$⊢3\cdot 3+0+0=9+0$$
273	234	addridi	$$⊢9+0=9$$
274	272 273	eqtri	$$⊢3\cdot 3+0+0=9$$
275	99	oveq1i	$$⊢2\cdot 3+1=6+1$$
276	35	dec0h	$$⊢7=07$$
277	275 216 276	3eqtri	$$⊢2\cdot 3+1=07$$
278	29 4 39 10 259 270 29 35 39 274 277	decmac	$$⊢32\cdot 3+0+1=97$$
279		4t3e12	$$⊢4\cdot 3=12$$
280		4p2e6	$$⊢4+2=6$$
281	206 57 280	addcomli	$$⊢2+4=6$$
282	10 4 30 279 281	decaddi	$$⊢4\cdot 3+4=16$$
283	33 30 39 30 252 210 29 3 10 278 282	decmac	$$⊢324\cdot 3+4=976$$
284	10 29 246 30 248 249 34 3 250 269 283	decma2c	$$⊢324\cdot 13+194=4406$$
285		6t3e18	$$⊢6\cdot 3=18$$
286	61 187 285	mulcomli	$$⊢3\cdot 6=18$$
287	10 14 18 286	decsuc	$$⊢3\cdot 6+1=19$$
288	10 4 4 63 113	decaddi	$$⊢2\cdot 6+2=14$$
289	29 4 4 259 3 30 10 287 288	decrmac	$$⊢32\cdot 6+2=194$$
290		6t4e24	$$⊢6\cdot 4=24$$
291	61 206 290	mulcomli	$$⊢4\cdot 6=24$$
292	3 33 30 252 30 4 289 291	decmul1c	$$⊢324\cdot 6=1944$$
293	34 37 3 245 30 247 284 292	decmul2c	$$⊢324\cdot 136=44064$$
294	244 293	eqtr4i	$$⊢34\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+N-1=324\cdot 136$$
295	26 2 28 32 34 23 36 38 176 177 184 294	modxai	$$⊢2^{629}\mathrm{mod}N=\left(N-1\right)\mathrm{mod}N$$
296		eqid	$$⊢629=629$$
297		eqid	$$⊢62=62$$
298	137	oveq2i	$$⊢2\cdot 6+0+0=2\cdot 6+0$$
299	63	oveq1i	$$⊢2\cdot 6+0=12+0$$
300	11	nn0cni	$$⊢12\in ℂ$$
301	300	addridi	$$⊢12+0=12$$
302	298 299 301	3eqtri	$$⊢2\cdot 6+0+0=12$$
303	12	dec0h	$$⊢5=05$$
304	81 55 303	3eqtri	$$⊢2\cdot 2+1=05$$
305	3 4 39 10 297 136 4 12 39 302 304	decma2c	$$⊢2\cdot 62+1=125$$
306		9t2e18	$$⊢9\cdot 2=18$$
307	234 57 306	mulcomli	$$⊢2\cdot 9=18$$
308	4 5 6 296 14 10 305 307	decmul2c	$$⊢2\cdot 629=1258$$
309	308 22	eqtr4i	$$⊢2\cdot 629=N-1$$
310		npcan	$$⊢\left(N\in ℂ\wedge 1\in ℂ\right)\to N-1+1=N$$
311	67 17 310	mp2an	$$⊢N-1+1=N$$
312	68	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=0+1$$
313	143 312 159	3eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=1\cdot 1$$
314	2 7 8 9 10 23 295 309 311 313	mod2xnegi	$$⊢2^{N-1}\mathrm{mod}N=1\mathrm{mod}N$$