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		3cn	$$⊢3\in ℂ$$
100		3t2e6	$$⊢3\cdot 2=6$$
101	99 57 100	mulcomli	$$⊢2\cdot 3=6$$
102	3	dec0h	$$⊢6=06$$
103	101 102	eqtri	$$⊢2\cdot 3=06$$
104	4 46 29 87 3 39 98 103	decmul2c	$$⊢2\cdot 153=306$$
105	67	mullidi	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
106	105 1	eqtri	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=1259$$
107		eqid	$$⊢1241=1241$$
108	4 30	deccl	$$⊢24\in {\mathbb{N}}_0$$
109		eqid	$$⊢24=24$$
110	4 30 55 109	decsuc	$$⊢24+1=25$$
111		eqid	$$⊢125=125$$
112		eqid	$$⊢124=124$$
113		eqid	$$⊢12=12$$
114		1p1e2	$$⊢1+1=2$$
115		2p2e4	$$⊢2+2=4$$
116	10 4 10 4 113 113 114 115	decadd	$$⊢12+12=24$$
117		5p4e9	$$⊢5+4=9$$
118	11 12 11 30 111 112 116 117	decadd	$$⊢125+124=249$$
119	108 110 118	decsucc	$$⊢125+124+1=250$$
120		9p1e10	$$⊢9+1=10$$
121	13 6 44 10 106 107 119 120	decaddc2	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1241=2500$$
122		eqid	$$⊢50=50$$
123	92	mul02i	$$⊢0\cdot 5=0$$
124	12 12 39 122 70 123	decmul1	$$⊢50\cdot 5=250$$
125	124	oveq1i	$$⊢50\cdot 5+0=250+0$$
126	51 39	deccl	$$⊢250\in {\mathbb{N}}_0$$
127	126	nn0cni	$$⊢250\in ℂ$$
128	127	addridi	$$⊢250+0=250$$
129	125 128	eqtri	$$⊢50\cdot 5+0=250$$
130	76	mul01i	$$⊢50\cdot 0=0$$
131	39	dec0h	$$⊢0=00$$
132	130 131	eqtri	$$⊢50\cdot 0=00$$
133	49 12 39 122 39 39 129 132	decmul2c	$$⊢50\cdot 50=2500$$
134	121 133	eqtr4i	$$⊢1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1241=50\cdot 50$$
135	26 2 47 48 49 45 86 104 134	mod2xi	$$⊢2^{306}\mathrm{mod}N=1241\mathrm{mod}N$$
136		eqid	$$⊢306=306$$
137		eqid	$$⊢30=30$$
138	10	dec0h	$$⊢1=01$$
139		00id	$$⊢0+0=0$$
140	101 139	oveq12i	$$⊢2\cdot 3+0+0=6+0$$
141	61	addridi	$$⊢6+0=6$$
142	140 141	eqtri	$$⊢2\cdot 3+0+0=6$$
143	57	mul01i	$$⊢2\cdot 0=0$$
144	143	oveq1i	$$⊢2\cdot 0+1=0+1$$
145		0p1e1	$$⊢0+1=1$$
146	144 145 138	3eqtri	$$⊢2\cdot 0+1=01$$
147	29 39 39 10 137 138 4 10 39 142 146	decma2c	$$⊢2\cdot 30+1=61$$
148	4 40 3 136 4 10 147 63	decmul2c	$$⊢2\cdot 306=612$$
149		eqid	$$⊢18=18$$
150	11 30 55 112	decsuc	$$⊢124+1=125$$
151		8cn	$$⊢8\in ℂ$$
152	151 17 18	addcomli	$$⊢1+8=9$$
153	44 10 10 14 107 149 150 152	decadd	$$⊢1241+18=1259$$
154	153 1	eqtr4i	$$⊢1241+18=N$$
155	34	nn0cni	$$⊢324\in ℂ$$
156	155	addlidi	$$⊢0+324=324$$
157	68	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+324=0+324$$
158	10 14	deccl	$$⊢18\in {\mathbb{N}}_0$$
159	10 30	deccl	$$⊢14\in {\mathbb{N}}_0$$
160		eqid	$$⊢14=14$$
161	17	mulridi	$$⊢1\cdot 1=1$$
162	161 114	oveq12i	$$⊢1\cdot 1+1+1=1+2$$
163		1p2e3	$$⊢1+2=3$$
164	162 163	eqtri	$$⊢1\cdot 1+1+1=3$$
165	151	mulridi	$$⊢8\cdot 1=8$$
166	165	oveq1i	$$⊢8\cdot 1+4=8+4$$
167		8p4e12	$$⊢8+4=12$$
168	166 167	eqtri	$$⊢8\cdot 1+4=12$$
169	10 14 10 30 149 160 10 4 10 164 168	decmac	$$⊢18\cdot 1+14=32$$
170	151	mullidi	$$⊢1\cdot 8=8$$
171	170	oveq1i	$$⊢1\cdot 8+6=8+6$$
172		8p6e14	$$⊢8+6=14$$
173	171 172	eqtri	$$⊢1\cdot 8+6=14$$
174		8t8e64	$$⊢8\cdot 8=64$$
175	14 10 14 149 30 3 173 174	decmul1c	$$⊢18\cdot 8=144$$
176	158 10 14 149 30 159 169 175	decmul2c	$$⊢18\cdot 18=324$$
177	156 157 176	3eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+324=18\cdot 18$$
178	2 41 8 43 34 45 135 148 154 177	mod2xnegi	$$⊢2^{612}\mathrm{mod}N=324\mathrm{mod}N$$
179	1	1259lem1	$$⊢2^{17}\mathrm{mod}N=136\mathrm{mod}N$$
180		eqid	$$⊢612=612$$
181		eqid	$$⊢17=17$$
182		eqid	$$⊢61=61$$
183	3 10 114 182	decsuc	$$⊢61+1=62$$
184		7p2e9	$$⊢7+2=9$$
185	56 57 184	addcomli	$$⊢2+7=9$$
186	27 4 10 35 180 181 183 185	decadd	$$⊢612+17=629$$
187	29 10	deccl	$$⊢31\in {\mathbb{N}}_0$$
188		eqid	$$⊢31=31$$
189		3p2e5	$$⊢3+2=5$$
190	99 57 189	addcomli	$$⊢2+3=5$$
191	10 4 29 113 190	decaddi	$$⊢12+3=15$$
192		5p1e6	$$⊢5+1=6$$
193	11 12 29 10 111 188 191 192	decadd	$$⊢125+31=156$$
194	114	oveq1i	$$⊢1+1+1=2+1$$
195	194 73	eqtri	$$⊢1+1+1=3$$
196		7p5e12	$$⊢7+5=12$$
197	56 92 196	addcomli	$$⊢5+7=12$$
198	10 12 10 35 88 181 195 4 197	decaddc	$$⊢15+17=32$$
199		eqid	$$⊢34=34$$
200		7p3e10	$$⊢7+3=10$$
201	56 99 200	addcomli	$$⊢3+7=10$$
202	99	mulridi	$$⊢3\cdot 1=3$$
203	17	addridi	$$⊢1+0=1$$
204	202 203	oveq12i	$$⊢3\cdot 1+1+0=3+1$$
205		3p1e4	$$⊢3+1=4$$
206	204 205	eqtri	$$⊢3\cdot 1+1+0=4$$
207		4cn	$$⊢4\in ℂ$$
208	207	mulridi	$$⊢4\cdot 1=4$$
209	208	oveq1i	$$⊢4\cdot 1+0=4+0$$
210	207	addridi	$$⊢4+0=4$$
211	30	dec0h	$$⊢4=04$$
212	209 210 211	3eqtri	$$⊢4\cdot 1+0=04$$
213	29 30 10 39 199 201 10 30 39 206 212	decmac	$$⊢34\cdot 1+3+7=44$$
214	4	dec0h	$$⊢2=02$$
215	100 145	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 199 214 4 39 10 217 221	decmac	$$⊢34\cdot 2+2=70$$
223	10 4 29 4 113 198 31 39 35 213 222	decma2c	$$⊢34\cdot 12+15+17=440$$
224		5t3e15	$$⊢5\cdot 3=15$$
225	92 99 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 207 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 199 12 3 4 227 231	decrmac	$$⊢34\cdot 5+6=176$$
233	11 12 46 3 111 193 31 3 36 223 232	decma2c	$$⊢34\cdot 125+125+31=4406$$
234		9cn	$$⊢9\in ℂ$$
235		9t3e27	$$⊢9\cdot 3=27$$
236	234 99 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 207 239	mulcomli	$$⊢4\cdot 9=36$$
241	151 61 172	addcomli	$$⊢6+8=14$$
242	29 3 14 240 205 30 241	decaddci	$$⊢4\cdot 9+8=44$$
243	29 30 14 199 6 30 30 238 242	decrmac	$$⊢34\cdot 9+8=314$$
244	13 6 13 14 1 22 31 30 187 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 120	addcomli	$$⊢1+9=10$$
256	10 39 145 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 114 260	decsuc	$$⊢11+1=12$$
262	89	oveq1i	$$⊢2\cdot 1+2=2+2$$
263	262 115 211	3eqtri	$$⊢2\cdot 1+2=04$$
264	29 4 10 4 259 261 10 30 39 206 263	decmac	$$⊢32\cdot 1+11+1=44$$
265	208	oveq1i	$$⊢4\cdot 1+6=4+6$$
266		6p4e10	$$⊢6+4=10$$
267	61 207 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	145 138	eqtri	$$⊢0+1=01$$
271		3t3e9	$$⊢3\cdot 3=9$$
272	271 139	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	101	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	207 57 280	addcomli	$$⊢2+4=6$$
282	10 4 30 279 281	decaddi	$$⊢4\cdot 3+4=16$$
283	33 30 39 30 252 211 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 99 285	mulcomli	$$⊢3\cdot 6=18$$
287	10 14 18 286	decsuc	$$⊢3\cdot 6+1=19$$
288	10 4 4 63 115	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 207 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 178 179 186 294	modxai	$$⊢2^{629}\mathrm{mod}N=\left(N-1\right)\mathrm{mod}N$$
296		eqid	$$⊢629=629$$
297		eqid	$$⊢62=62$$
298	139	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 138 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	145 312 161	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$$