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