Metamath Proof Explorer

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 addridi 
 |-  ( ; ; 1 1 6 + 0 ) = ; ; 1 1 6
74 eqid 
 |-  ; 2 5 = ; 2 5
75 52 nn0cni 
 |-  ; 1 1 e. CC
76 75 addridi 
 |-  ( ; 1 1 + 0 ) = ; 1 1
77 2cn 
 |-  2 e. CC
78 77 mullidi 
 |-  ( 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 mullidi 
 |-  ( 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 addlidi 
 |-  ( 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 mullidi 
 |-  ( 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 addlidi 
 |-  ( 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 addridi 
 |-  ( ; 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 addlidi 
 |-  ( 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 addlidi 
 |-  ( 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 addlidi 
 |-  ( 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 addlidi 
 |-  ( 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 addridi 
 |-  ( ; 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 mulridi 
 |-  ( 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 addridi 
 |-  ( 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 mullidi 
 |-  ( 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 mulridi 
 |-  ( ; ; ; 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 addridi 
 |-  ( 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 addridi 
 |-  ( ; 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 mulridi 
 |-  ( ; ; 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 addlidi 
 |-  ( 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 addlidi 
 |-  ( 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 mulridi 
 |-  ( 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 mulridi 
 |-  ( 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 mullidi 
 |-  ( 1 x. 9 ) = 9
405 161 addlidi 
 |-  ( 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 mullidi 
 |-  ( 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 addridi 
 |-  ( 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 mulridi 
 |-  ( ; 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 addridi 
 |-  ( ; 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 addridi 
 |-  ( 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 addlidi 
 |-  ( 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 addridi 
 |-  ( ; ; 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 addlidi 
 |-  ( 0 + 5 ) = 5
528 5 11 3 16 216 526 527 409 decadd 
 |-  ( 1 + ; 5 4 ) = ; 5 5
529 83 addridi 
 |-  ( 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 addridi 
 |-  ( ; 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 addridi 
 |-  ( ; ; 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 addridi 
 |-  ( 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 addlidi 
 |-  ( 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 addridi 
 |-  ( ; ; ; 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 mullidi 
 |-  ( 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 mullidi 
 |-  ( 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 )