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 = ; ; ; 2 5 0 3
Assertion	2503lem2	|- ( ( 2 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )

Proof

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