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 ⊢ 𝑁 = 2 5 0 3
Assertion 2503lem2 ( ( 2 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 )

Proof

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