# 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 = 2503$
Assertion 2503lem2 $⊢ 2 N − 1 mod N = 1 mod N$

### Proof

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