Metamath Proof Explorer

Theorem 1259lem4

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

Ref Expression
Hypothesis 1259prm.1 ⊢ 𝑁 = 1 2 5 9
Assertion 1259lem4 ( ( 2 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 )

Proof

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