Metamath Proof Explorer

Theorem 4001lem1

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

Ref Expression
Hypothesis 4001prm.1 ⊢ 𝑁 = 4 0 0 1
Assertion 4001lem1 ( ( 2 ↑ 2 0 0 ) mod 𝑁 ) = ( 9 0 2 mod 𝑁 )

Proof

Step Hyp Ref Expression
1 4001prm.1 ⊢ 𝑁 = 4 0 0 1
2 4nn0 ⊢ 4 ∈ ℕ0
3 0nn0 ⊢ 0 ∈ ℕ0
4 2 3 deccl ⊢ 4 0 ∈ ℕ0
5 4 3 deccl ⊢ 4 0 0 ∈ ℕ0
6 1nn ⊢ 1 ∈ ℕ
7 5 6 decnncl ⊢ 4 0 0 1 ∈ ℕ
8 1 7 eqeltri ⊢ 𝑁 ∈ ℕ
9 2nn ⊢ 2 ∈ ℕ
10 10nn0 ⊢ 1 0 ∈ ℕ0
11 10 3 deccl ⊢ 1 0 0 ∈ ℕ0
12 9nn0 ⊢ 9 ∈ ℕ0
13 12 2 deccl ⊢ 9 4 ∈ ℕ0
14 13 nn0zi ⊢ 9 4 ∈ ℤ
15 6nn0 ⊢ 6 ∈ ℕ0
16 1nn0 ⊢ 1 ∈ ℕ0
17 15 16 deccl ⊢ 6 1 ∈ ℕ0
18 17 2 deccl ⊢ 6 1 4 ∈ ℕ0
19 12 3 deccl ⊢ 9 0 ∈ ℕ0
20 2nn0 ⊢ 2 ∈ ℕ0
21 19 20 deccl ⊢ 9 0 2 ∈ ℕ0
22 5nn0 ⊢ 5 ∈ ℕ0
23 22 3 deccl ⊢ 5 0 ∈ ℕ0
24 8nn0 ⊢ 8 ∈ ℕ0
25 20 24 deccl ⊢ 2 8 ∈ ℕ0
26 25 15 deccl ⊢ 2 8 6 ∈ ℕ0
27 26 nn0zi ⊢ 2 8 6 ∈ ℤ
28 7nn0 ⊢ 7 ∈ ℕ0
29 10 28 deccl ⊢ 1 0 7 ∈ ℕ0
30 29 3 deccl ⊢ 1 0 7 0 ∈ ℕ0
31 20 22 deccl ⊢ 2 5 ∈ ℕ0
32 10 2 deccl ⊢ 1 0 4 ∈ ℕ0
33 32 15 deccl ⊢ 1 0 4 6 ∈ ℕ0
34 33 nn0zi ⊢ 1 0 4 6 ∈ ℤ
35 20 3 deccl ⊢ 2 0 ∈ ℕ0
36 35 2 deccl ⊢ 2 0 4 ∈ ℕ0
37 36 15 deccl ⊢ 2 0 4 6 ∈ ℕ0
38 20 2 deccl ⊢ 2 4 ∈ ℕ0
39 0z ⊢ 0 ∈ ℤ
40 10 20 deccl ⊢ 1 0 2 ∈ ℕ0
41 3nn0 ⊢ 3 ∈ ℕ0
42 40 41 deccl ⊢ 1 0 2 3 ∈ ℕ0
43 16 20 deccl ⊢ 1 2 ∈ ℕ0
44 2z ⊢ 2 ∈ ℤ
45 12 22 deccl ⊢ 9 5 ∈ ℕ0
46 1z ⊢ 1 ∈ ℤ
47 15 2 deccl ⊢ 6 4 ∈ ℕ0
48 2exp6 ⊢ ( 2 ↑ 6 ) = 6 4
49 48 oveq1i ⊢ ( ( 2 ↑ 6 ) mod 𝑁 ) = ( 6 4 mod 𝑁 )
50 6cn ⊢ 6 ∈ ℂ
51 2cn ⊢ 2 ∈ ℂ
52 6t2e12 ⊢ ( 6 · 2 ) = 1 2
53 50 51 52 mulcomli ⊢ ( 2 · 6 ) = 1 2
54 eqid ⊢ 9 5 = 9 5
55 eqid ⊢ 4 0 0 = 4 0 0
56 9cn ⊢ 9 ∈ ℂ
57 56 addridi ⊢ ( 9 + 0 ) = 9
58 12 dec0h ⊢ 9 = 0 9
59 57 58 eqtri ⊢ ( 9 + 0 ) = 0 9
60 eqid ⊢ 4 0 = 4 0
61 00id ⊢ ( 0 + 0 ) = 0
62 3 dec0h ⊢ 0 = 0 0
63 61 62 eqtri ⊢ ( 0 + 0 ) = 0 0
64 4cn ⊢ 4 ∈ ℂ
65 64 mullidi ⊢ ( 1 · 4 ) = 4
66 65 61 oveq12i ⊢ ( ( 1 · 4 ) + ( 0 + 0 ) ) = ( 4 + 0 )
67 64 addridi ⊢ ( 4 + 0 ) = 4
68 66 67 eqtri ⊢ ( ( 1 · 4 ) + ( 0 + 0 ) ) = 4
69 ax-1cn ⊢ 1 ∈ ℂ
70 69 mul01i ⊢ ( 1 · 0 ) = 0
71 70 oveq1i ⊢ ( ( 1 · 0 ) + 0 ) = ( 0 + 0 )
72 71 61 62 3eqtri ⊢ ( ( 1 · 0 ) + 0 ) = 0 0
73 2 3 3 3 60 63 16 3 3 68 72 decma2c ⊢ ( ( 1 · 4 0 ) + ( 0 + 0 ) ) = 4 0
74 70 oveq1i ⊢ ( ( 1 · 0 ) + 9 ) = ( 0 + 9 )
75 56 addlidi ⊢ ( 0 + 9 ) = 9
76 74 75 58 3eqtri ⊢ ( ( 1 · 0 ) + 9 ) = 0 9
77 4 3 3 12 55 59 16 12 3 73 76 decma2c ⊢ ( ( 1 · 4 0 0 ) + ( 9 + 0 ) ) = 4 0 9
78 69 mulridi ⊢ ( 1 · 1 ) = 1
79 78 oveq1i ⊢ ( ( 1 · 1 ) + 5 ) = ( 1 + 5 )
80 5cn ⊢ 5 ∈ ℂ
81 5p1e6 ⊢ ( 5 + 1 ) = 6
82 80 69 81 addcomli ⊢ ( 1 + 5 ) = 6
83 15 dec0h ⊢ 6 = 0 6
84 79 82 83 3eqtri ⊢ ( ( 1 · 1 ) + 5 ) = 0 6
85 5 16 12 22 1 54 16 15 3 77 84 decma2c ⊢ ( ( 1 · 𝑁 ) + 9 5 ) = 4 0 9 6
86 eqid ⊢ 6 4 = 6 4
87 eqid ⊢ 2 5 = 2 5
88 2p2e4 ⊢ ( 2 + 2 ) = 4
89 88 oveq2i ⊢ ( ( 6 · 6 ) + ( 2 + 2 ) ) = ( ( 6 · 6 ) + 4 )
90 6t6e36 ⊢ ( 6 · 6 ) = 3 6
91 3p1e4 ⊢ ( 3 + 1 ) = 4
92 6p4e10 ⊢ ( 6 + 4 ) = 1 0
93 41 15 2 90 91 92 decaddci2 ⊢ ( ( 6 · 6 ) + 4 ) = 4 0
94 89 93 eqtri ⊢ ( ( 6 · 6 ) + ( 2 + 2 ) ) = 4 0
95 6t4e24 ⊢ ( 6 · 4 ) = 2 4
96 50 64 95 mulcomli ⊢ ( 4 · 6 ) = 2 4
97 5p4e9 ⊢ ( 5 + 4 ) = 9
98 80 64 97 addcomli ⊢ ( 4 + 5 ) = 9
99 20 2 22 96 98 decaddi ⊢ ( ( 4 · 6 ) + 5 ) = 2 9
100 15 2 20 22 86 87 15 12 20 94 99 decmac ⊢ ( ( 6 4 · 6 ) + 2 5 ) = 4 0 9
101 4p1e5 ⊢ ( 4 + 1 ) = 5
102 20 2 101 95 decsuc ⊢ ( ( 6 · 4 ) + 1 ) = 2 5
103 4t4e16 ⊢ ( 4 · 4 ) = 1 6
104 2 15 2 86 15 16 102 103 decmul1c ⊢ ( 6 4 · 4 ) = 2 5 6
105 47 15 2 86 15 31 100 104 decmul2c ⊢ ( 6 4 · 6 4 ) = 4 0 9 6
106 85 105 eqtr4i ⊢ ( ( 1 · 𝑁 ) + 9 5 ) = ( 6 4 · 6 4 )
107 8 9 15 46 47 45 49 53 106 mod2xi ⊢ ( ( 2 ↑ 1 2 ) mod 𝑁 ) = ( 9 5 mod 𝑁 )
108 eqid ⊢ 1 2 = 1 2
109 51 mulridi ⊢ ( 2 · 1 ) = 2
110 109 oveq1i ⊢ ( ( 2 · 1 ) + 0 ) = ( 2 + 0 )
111 51 addridi ⊢ ( 2 + 0 ) = 2
112 110 111 eqtri ⊢ ( ( 2 · 1 ) + 0 ) = 2
113 2t2e4 ⊢ ( 2 · 2 ) = 4
114 2 dec0h ⊢ 4 = 0 4
115 113 114 eqtri ⊢ ( 2 · 2 ) = 0 4
116 20 16 20 108 2 3 112 115 decmul2c ⊢ ( 2 · 1 2 ) = 2 4
117 eqid ⊢ 1 0 2 3 = 1 0 2 3
118 40 nn0cni ⊢ 1 0 2 ∈ ℂ
119 118 addridi ⊢ ( 1 0 2 + 0 ) = 1 0 2
120 dec10p ⊢ ( 1 0 + 0 ) = 1 0
121 4t2e8 ⊢ ( 4 · 2 ) = 8
122 64 51 121 mulcomli ⊢ ( 2 · 4 ) = 8
123 69 addridi ⊢ ( 1 + 0 ) = 1
124 122 123 oveq12i ⊢ ( ( 2 · 4 ) + ( 1 + 0 ) ) = ( 8 + 1 )
125 8p1e9 ⊢ ( 8 + 1 ) = 9
126 124 125 eqtri ⊢ ( ( 2 · 4 ) + ( 1 + 0 ) ) = 9
127 51 mul01i ⊢ ( 2 · 0 ) = 0
128 127 oveq1i ⊢ ( ( 2 · 0 ) + 0 ) = ( 0 + 0 )
129 128 61 62 3eqtri ⊢ ( ( 2 · 0 ) + 0 ) = 0 0
130 2 3 16 3 60 120 20 3 3 126 129 decma2c ⊢ ( ( 2 · 4 0 ) + ( 1 0 + 0 ) ) = 9 0
131 127 oveq1i ⊢ ( ( 2 · 0 ) + 2 ) = ( 0 + 2 )
132 51 addlidi ⊢ ( 0 + 2 ) = 2
133 20 dec0h ⊢ 2 = 0 2
134 131 132 133 3eqtri ⊢ ( ( 2 · 0 ) + 2 ) = 0 2
135 4 3 10 20 55 119 20 20 3 130 134 decma2c ⊢ ( ( 2 · 4 0 0 ) + ( 1 0 2 + 0 ) ) = 9 0 2
136 109 oveq1i ⊢ ( ( 2 · 1 ) + 3 ) = ( 2 + 3 )
137 3cn ⊢ 3 ∈ ℂ
138 3p2e5 ⊢ ( 3 + 2 ) = 5
139 137 51 138 addcomli ⊢ ( 2 + 3 ) = 5
140 22 dec0h ⊢ 5 = 0 5
141 136 139 140 3eqtri ⊢ ( ( 2 · 1 ) + 3 ) = 0 5
142 5 16 40 41 1 117 20 22 3 135 141 decma2c ⊢ ( ( 2 · 𝑁 ) + 1 0 2 3 ) = 9 0 2 5
143 2 28 deccl ⊢ 4 7 ∈ ℕ0
144 eqid ⊢ 4 7 = 4 7
145 98 oveq2i ⊢ ( ( 9 · 9 ) + ( 4 + 5 ) ) = ( ( 9 · 9 ) + 9 )
146 9t9e81 ⊢ ( 9 · 9 ) = 8 1
147 9p1e10 ⊢ ( 9 + 1 ) = 1 0
148 56 69 147 addcomli ⊢ ( 1 + 9 ) = 1 0
149 24 16 12 146 125 148 decaddci2 ⊢ ( ( 9 · 9 ) + 9 ) = 9 0
150 145 149 eqtri ⊢ ( ( 9 · 9 ) + ( 4 + 5 ) ) = 9 0
151 9t5e45 ⊢ ( 9 · 5 ) = 4 5
152 56 80 151 mulcomli ⊢ ( 5 · 9 ) = 4 5
153 7cn ⊢ 7 ∈ ℂ
154 7p5e12 ⊢ ( 7 + 5 ) = 1 2
155 153 80 154 addcomli ⊢ ( 5 + 7 ) = 1 2
156 2 22 28 152 101 20 155 decaddci ⊢ ( ( 5 · 9 ) + 7 ) = 5 2
157 12 22 2 28 54 144 12 20 22 150 156 decmac ⊢ ( ( 9 5 · 9 ) + 4 7 ) = 9 0 2
158 5p2e7 ⊢ ( 5 + 2 ) = 7
159 2 22 20 151 158 decaddi ⊢ ( ( 9 · 5 ) + 2 ) = 4 7
160 5t5e25 ⊢ ( 5 · 5 ) = 2 5
161 22 12 22 54 22 20 159 160 decmul1c ⊢ ( 9 5 · 5 ) = 4 7 5
162 45 12 22 54 22 143 157 161 decmul2c ⊢ ( 9 5 · 9 5 ) = 9 0 2 5
163 142 162 eqtr4i ⊢ ( ( 2 · 𝑁 ) + 1 0 2 3 ) = ( 9 5 · 9 5 )
164 8 9 43 44 45 42 107 116 163 mod2xi ⊢ ( ( 2 ↑ 2 4 ) mod 𝑁 ) = ( 1 0 2 3 mod 𝑁 )
165 eqid ⊢ 2 4 = 2 4
166 20 2 101 165 decsuc ⊢ ( 2 4 + 1 ) = 2 5
167 37 nn0cni ⊢ 2 0 4 6 ∈ ℂ
168 167 addlidi ⊢ ( 0 + 2 0 4 6 ) = 2 0 4 6
169 8 nncni ⊢ 𝑁 ∈ ℂ
170 169 mul02i ⊢ ( 0 · 𝑁 ) = 0
171 170 oveq1i ⊢ ( ( 0 · 𝑁 ) + 2 0 4 6 ) = ( 0 + 2 0 4 6 )
172 eqid ⊢ 1 0 2 = 1 0 2
173 20 dec0u ⊢ ( 1 0 · 2 ) = 2 0
174 20 10 20 172 173 113 decmul1 ⊢ ( 1 0 2 · 2 ) = 2 0 4
175 3t2e6 ⊢ ( 3 · 2 ) = 6
176 20 40 41 117 174 175 decmul1 ⊢ ( 1 0 2 3 · 2 ) = 2 0 4 6
177 168 171 176 3eqtr4i ⊢ ( ( 0 · 𝑁 ) + 2 0 4 6 ) = ( 1 0 2 3 · 2 )
178 8 9 38 39 42 37 164 166 177 modxp1i ⊢ ( ( 2 ↑ 2 5 ) mod 𝑁 ) = ( 2 0 4 6 mod 𝑁 )
179 113 oveq1i ⊢ ( ( 2 · 2 ) + 1 ) = ( 4 + 1 )
180 179 101 eqtri ⊢ ( ( 2 · 2 ) + 1 ) = 5
181 5t2e10 ⊢ ( 5 · 2 ) = 1 0
182 80 51 181 mulcomli ⊢ ( 2 · 5 ) = 1 0
183 20 20 22 87 3 16 180 182 decmul2c ⊢ ( 2 · 2 5 ) = 5 0
184 eqid ⊢ 1 0 7 0 = 1 0 7 0
185 20 16 deccl ⊢ 2 1 ∈ ℕ0
186 eqid ⊢ 1 0 7 = 1 0 7
187 eqid ⊢ 1 0 4 = 1 0 4
188 0p1e1 ⊢ ( 0 + 1 ) = 1
189 10p10e20 ⊢ ( 1 0 + 1 0 ) = 2 0
190 20 3 188 189 decsuc ⊢ ( ( 1 0 + 1 0 ) + 1 ) = 2 1
191 7p4e11 ⊢ ( 7 + 4 ) = 1 1
192 10 28 10 2 186 187 190 16 191 decaddc ⊢ ( 1 0 7 + 1 0 4 ) = 2 1 1
193 185 nn0cni ⊢ 2 1 ∈ ℂ
194 193 addridi ⊢ ( 2 1 + 0 ) = 2 1
195 111 20 eqeltri ⊢ ( 2 + 0 ) ∈ ℕ0
196 eqid ⊢ 1 0 4 6 = 1 0 4 6
197 dfdec10 ⊢ 4 1 = ( ( 1 0 · 4 ) + 1 )
198 197 eqcomi ⊢ ( ( 1 0 · 4 ) + 1 ) = 4 1
199 6p2e8 ⊢ ( 6 + 2 ) = 8
200 16 15 20 103 199 decaddi ⊢ ( ( 4 · 4 ) + 2 ) = 1 8
201 10 2 20 187 2 24 16 198 200 decrmac ⊢ ( ( 1 0 4 · 4 ) + 2 ) = 4 1 8
202 95 111 oveq12i ⊢ ( ( 6 · 4 ) + ( 2 + 0 ) ) = ( 2 4 + 2 )
203 4p2e6 ⊢ ( 4 + 2 ) = 6
204 20 2 20 165 203 decaddi ⊢ ( 2 4 + 2 ) = 2 6
205 202 204 eqtri ⊢ ( ( 6 · 4 ) + ( 2 + 0 ) ) = 2 6
206 32 15 195 196 2 15 20 201 205 decrmac ⊢ ( ( 1 0 4 6 · 4 ) + ( 2 + 0 ) ) = 4 1 8 6
207 33 nn0cni ⊢ 1 0 4 6 ∈ ℂ
208 207 mul01i ⊢ ( 1 0 4 6 · 0 ) = 0
209 208 oveq1i ⊢ ( ( 1 0 4 6 · 0 ) + 1 ) = ( 0 + 1 )
210 16 dec0h ⊢ 1 = 0 1
211 209 188 210 3eqtri ⊢ ( ( 1 0 4 6 · 0 ) + 1 ) = 0 1
212 2 3 20 16 60 194 33 16 3 206 211 decma2c ⊢ ( ( 1 0 4 6 · 4 0 ) + ( 2 1 + 0 ) ) = 4 1 8 6 1
213 4 3 185 16 55 192 33 16 3 212 211 decma2c ⊢ ( ( 1 0 4 6 · 4 0 0 ) + ( 1 0 7 + 1 0 4 ) ) = 4 1 8 6 1 1
214 207 mulridi ⊢ ( 1 0 4 6 · 1 ) = 1 0 4 6
215 214 oveq1i ⊢ ( ( 1 0 4 6 · 1 ) + 0 ) = ( 1 0 4 6 + 0 )
216 207 addridi ⊢ ( 1 0 4 6 + 0 ) = 1 0 4 6
217 215 216 eqtri ⊢ ( ( 1 0 4 6 · 1 ) + 0 ) = 1 0 4 6
218 5 16 29 3 1 184 33 15 32 213 217 decma2c ⊢ ( ( 1 0 4 6 · 𝑁 ) + 1 0 7 0 ) = 4 1 8 6 1 1 6
219 eqid ⊢ 2 0 4 6 = 2 0 4 6
220 43 20 deccl ⊢ 1 2 2 ∈ ℕ0
221 220 28 deccl ⊢ 1 2 2 7 ∈ ℕ0
222 eqid ⊢ 2 0 4 = 2 0 4
223 eqid ⊢ 1 2 2 7 = 1 2 2 7
224 24 16 deccl ⊢ 8 1 ∈ ℕ0
225 224 12 deccl ⊢ 8 1 9 ∈ ℕ0
226 eqid ⊢ 2 0 = 2 0
227 eqid ⊢ 1 2 2 = 1 2 2
228 eqid ⊢ 8 1 9 = 8 1 9
229 eqid ⊢ 8 1 = 8 1
230 8cn ⊢ 8 ∈ ℂ
231 230 69 125 addcomli ⊢ ( 1 + 8 ) = 9
232 2p1e3 ⊢ ( 2 + 1 ) = 3
233 16 20 24 16 108 229 231 232 decadd ⊢ ( 1 2 + 8 1 ) = 9 3
234 12 41 91 233 decsuc ⊢ ( ( 1 2 + 8 1 ) + 1 ) = 9 4
235 9p2e11 ⊢ ( 9 + 2 ) = 1 1
236 56 51 235 addcomli ⊢ ( 2 + 9 ) = 1 1
237 43 20 224 12 227 228 234 16 236 decaddc ⊢ ( 1 2 2 + 8 1 9 ) = 9 4 1
238 13 nn0cni ⊢ 9 4 ∈ ℂ
239 238 addridi ⊢ ( 9 4 + 0 ) = 9 4
240 123 16 eqeltri ⊢ ( 1 + 0 ) ∈ ℕ0
241 51 mul02i ⊢ ( 0 · 2 ) = 0
242 241 123 oveq12i ⊢ ( ( 0 · 2 ) + ( 1 + 0 ) ) = ( 0 + 1 )
243 242 188 eqtri ⊢ ( ( 0 · 2 ) + ( 1 + 0 ) ) = 1
244 20 3 240 226 20 113 243 decrmanc ⊢ ( ( 2 0 · 2 ) + ( 1 + 0 ) ) = 4 1
245 121 oveq1i ⊢ ( ( 4 · 2 ) + 0 ) = ( 8 + 0 )
246 230 addridi ⊢ ( 8 + 0 ) = 8
247 24 dec0h ⊢ 8 = 0 8
248 245 246 247 3eqtri ⊢ ( ( 4 · 2 ) + 0 ) = 0 8
249 35 2 16 3 222 147 20 24 3 244 248 decmac ⊢ ( ( 2 0 4 · 2 ) + ( 9 + 1 ) ) = 4 1 8
250 64 51 203 addcomli ⊢ ( 2 + 4 ) = 6
251 16 20 2 52 250 decaddi ⊢ ( ( 6 · 2 ) + 4 ) = 1 6
252 36 15 12 2 219 239 20 15 16 249 251 decmac ⊢ ( ( 2 0 4 6 · 2 ) + ( 9 4 + 0 ) ) = 4 1 8 6
253 167 mul01i ⊢ ( 2 0 4 6 · 0 ) = 0
254 253 oveq1i ⊢ ( ( 2 0 4 6 · 0 ) + 1 ) = ( 0 + 1 )
255 254 188 210 3eqtri ⊢ ( ( 2 0 4 6 · 0 ) + 1 ) = 0 1
256 20 3 13 16 226 237 37 16 3 252 255 decma2c ⊢ ( ( 2 0 4 6 · 2 0 ) + ( 1 2 2 + 8 1 9 ) ) = 4 1 8 6 1
257 41 dec0h ⊢ 3 = 0 3
258 188 16 eqeltri ⊢ ( 0 + 1 ) ∈ ℕ0
259 64 mul02i ⊢ ( 0 · 4 ) = 0
260 259 188 oveq12i ⊢ ( ( 0 · 4 ) + ( 0 + 1 ) ) = ( 0 + 1 )
261 260 188 eqtri ⊢ ( ( 0 · 4 ) + ( 0 + 1 ) ) = 1
262 20 3 258 226 2 122 261 decrmanc ⊢ ( ( 2 0 · 4 ) + ( 0 + 1 ) ) = 8 1
263 6p3e9 ⊢ ( 6 + 3 ) = 9
264 16 15 41 103 263 decaddi ⊢ ( ( 4 · 4 ) + 3 ) = 1 9
265 35 2 3 41 222 257 2 12 16 262 264 decmac ⊢ ( ( 2 0 4 · 4 ) + 3 ) = 8 1 9
266 153 64 191 addcomli ⊢ ( 4 + 7 ) = 1 1
267 20 2 28 95 232 16 266 decaddci ⊢ ( ( 6 · 4 ) + 7 ) = 3 1
268 36 15 28 219 2 16 41 265 267 decrmac ⊢ ( ( 2 0 4 6 · 4 ) + 7 ) = 8 1 9 1
269 35 2 220 28 222 223 37 16 225 256 268 decma2c ⊢ ( ( 2 0 4 6 · 2 0 4 ) + 1 2 2 7 ) = 4 1 8 6 1 1
270 50 mul02i ⊢ ( 0 · 6 ) = 0
271 270 oveq1i ⊢ ( ( 0 · 6 ) + 2 ) = ( 0 + 2 )
272 271 132 eqtri ⊢ ( ( 0 · 6 ) + 2 ) = 2
273 20 3 20 226 15 53 272 decrmanc ⊢ ( ( 2 0 · 6 ) + 2 ) = 1 2 2
274 4p3e7 ⊢ ( 4 + 3 ) = 7
275 20 2 41 96 274 decaddi ⊢ ( ( 4 · 6 ) + 3 ) = 2 7
276 35 2 41 222 15 28 20 273 275 decrmac ⊢ ( ( 2 0 4 · 6 ) + 3 ) = 1 2 2 7
277 15 36 15 219 15 41 276 90 decmul1c ⊢ ( 2 0 4 6 · 6 ) = 1 2 2 7 6
278 37 36 15 219 15 221 269 277 decmul2c ⊢ ( 2 0 4 6 · 2 0 4 6 ) = 4 1 8 6 1 1 6
279 218 278 eqtr4i ⊢ ( ( 1 0 4 6 · 𝑁 ) + 1 0 7 0 ) = ( 2 0 4 6 · 2 0 4 6 )
280 8 9 31 34 37 30 178 183 279 mod2xi ⊢ ( ( 2 ↑ 5 0 ) mod 𝑁 ) = ( 1 0 7 0 mod 𝑁 )
281 23 nn0cni ⊢ 5 0 ∈ ℂ
282 eqid ⊢ 5 0 = 5 0
283 20 22 3 282 181 241 decmul1 ⊢ ( 5 0 · 2 ) = 1 0 0
284 281 51 283 mulcomli ⊢ ( 2 · 5 0 ) = 1 0 0
285 eqid ⊢ 6 1 4 = 6 1 4
286 20 12 deccl ⊢ 2 9 ∈ ℕ0
287 eqid ⊢ 6 1 = 6 1
288 eqid ⊢ 2 9 = 2 9
289 199 oveq1i ⊢ ( ( 6 + 2 ) + 1 ) = ( 8 + 1 )
290 289 125 eqtri ⊢ ( ( 6 + 2 ) + 1 ) = 9
291 15 16 20 12 287 288 290 148 decaddc2 ⊢ ( 6 1 + 2 9 ) = 9 0
292 61 3 eqeltri ⊢ ( 0 + 0 ) ∈ ℕ0
293 eqid ⊢ 2 8 6 = 2 8 6
294 eqid ⊢ 2 8 = 2 8
295 122 oveq1i ⊢ ( ( 2 · 4 ) + 3 ) = ( 8 + 3 )
296 8p3e11 ⊢ ( 8 + 3 ) = 1 1
297 295 296 eqtri ⊢ ( ( 2 · 4 ) + 3 ) = 1 1
298 8t4e32 ⊢ ( 8 · 4 ) = 3 2
299 41 20 20 298 88 decaddi ⊢ ( ( 8 · 4 ) + 2 ) = 3 4
300 20 24 20 294 2 2 41 297 299 decrmac ⊢ ( ( 2 8 · 4 ) + 2 ) = 1 1 4
301 95 61 oveq12i ⊢ ( ( 6 · 4 ) + ( 0 + 0 ) ) = ( 2 4 + 0 )
302 38 nn0cni ⊢ 2 4 ∈ ℂ
303 302 addridi ⊢ ( 2 4 + 0 ) = 2 4
304 301 303 eqtri ⊢ ( ( 6 · 4 ) + ( 0 + 0 ) ) = 2 4
305 25 15 292 293 2 2 20 300 304 decrmac ⊢ ( ( 2 8 6 · 4 ) + ( 0 + 0 ) ) = 1 1 4 4
306 26 nn0cni ⊢ 2 8 6 ∈ ℂ
307 306 mul01i ⊢ ( 2 8 6 · 0 ) = 0
308 307 oveq1i ⊢ ( ( 2 8 6 · 0 ) + 9 ) = ( 0 + 9 )
309 308 75 58 3eqtri ⊢ ( ( 2 8 6 · 0 ) + 9 ) = 0 9
310 2 3 3 12 60 59 26 12 3 305 309 decma2c ⊢ ( ( 2 8 6 · 4 0 ) + ( 9 + 0 ) ) = 1 1 4 4 9
311 307 oveq1i ⊢ ( ( 2 8 6 · 0 ) + 0 ) = ( 0 + 0 )
312 311 61 62 3eqtri ⊢ ( ( 2 8 6 · 0 ) + 0 ) = 0 0
313 4 3 12 3 55 291 26 3 3 310 312 decma2c ⊢ ( ( 2 8 6 · 4 0 0 ) + ( 6 1 + 2 9 ) ) = 1 1 4 4 9 0
314 230 mulridi ⊢ ( 8 · 1 ) = 8
315 16 20 24 294 109 314 decmul1 ⊢ ( 2 8 · 1 ) = 2 8
316 20 24 125 315 decsuc ⊢ ( ( 2 8 · 1 ) + 1 ) = 2 9
317 50 mulridi ⊢ ( 6 · 1 ) = 6
318 317 oveq1i ⊢ ( ( 6 · 1 ) + 4 ) = ( 6 + 4 )
319 318 92 eqtri ⊢ ( ( 6 · 1 ) + 4 ) = 1 0
320 25 15 2 293 16 3 16 316 319 decrmac ⊢ ( ( 2 8 6 · 1 ) + 4 ) = 2 9 0
321 5 16 17 2 1 285 26 3 286 313 320 decma2c ⊢ ( ( 2 8 6 · 𝑁 ) + 6 1 4 ) = 1 1 4 4 9 0 0
322 16 16 deccl ⊢ 1 1 ∈ ℕ0
323 322 2 deccl ⊢ 1 1 4 ∈ ℕ0
324 323 2 deccl ⊢ 1 1 4 4 ∈ ℕ0
325 324 12 deccl ⊢ 1 1 4 4 9 ∈ ℕ0
326 28 2 deccl ⊢ 7 4 ∈ ℕ0
327 326 12 deccl ⊢ 7 4 9 ∈ ℕ0
328 eqid ⊢ 1 0 = 1 0
329 eqid ⊢ 7 4 9 = 7 4 9
330 326 nn0cni ⊢ 7 4 ∈ ℂ
331 330 addridi ⊢ ( 7 4 + 0 ) = 7 4
332 153 addridi ⊢ ( 7 + 0 ) = 7
333 332 28 eqeltri ⊢ ( 7 + 0 ) ∈ ℕ0
334 10 nn0cni ⊢ 1 0 ∈ ℂ
335 334 mulridi ⊢ ( 1 0 · 1 ) = 1 0
336 16 3 188 335 decsuc ⊢ ( ( 1 0 · 1 ) + 1 ) = 1 1
337 153 mulridi ⊢ ( 7 · 1 ) = 7
338 337 332 oveq12i ⊢ ( ( 7 · 1 ) + ( 7 + 0 ) ) = ( 7 + 7 )
339 7p7e14 ⊢ ( 7 + 7 ) = 1 4
340 338 339 eqtri ⊢ ( ( 7 · 1 ) + ( 7 + 0 ) ) = 1 4
341 10 28 333 186 16 2 16 336 340 decrmac ⊢ ( ( 1 0 7 · 1 ) + ( 7 + 0 ) ) = 1 1 4
342 69 mul02i ⊢ ( 0 · 1 ) = 0
343 342 oveq1i ⊢ ( ( 0 · 1 ) + 4 ) = ( 0 + 4 )
344 64 addlidi ⊢ ( 0 + 4 ) = 4
345 343 344 114 3eqtri ⊢ ( ( 0 · 1 ) + 4 ) = 0 4
346 29 3 28 2 184 331 16 2 3 341 345 decmac ⊢ ( ( 1 0 7 0 · 1 ) + ( 7 4 + 0 ) ) = 1 1 4 4
347 30 nn0cni ⊢ 1 0 7 0 ∈ ℂ
348 347 mul01i ⊢ ( 1 0 7 0 · 0 ) = 0
349 348 oveq1i ⊢ ( ( 1 0 7 0 · 0 ) + 9 ) = ( 0 + 9 )
350 349 75 58 3eqtri ⊢ ( ( 1 0 7 0 · 0 ) + 9 ) = 0 9
351 16 3 326 12 328 329 30 12 3 346 350 decma2c ⊢ ( ( 1 0 7 0 · 1 0 ) + 7 4 9 ) = 1 1 4 4 9
352 dfdec10 ⊢ 7 4 = ( ( 1 0 · 7 ) + 4 )
353 352 eqcomi ⊢ ( ( 1 0 · 7 ) + 4 ) = 7 4
354 7t7e49 ⊢ ( 7 · 7 ) = 4 9
355 28 10 28 186 12 2 353 354 decmul1c ⊢ ( 1 0 7 · 7 ) = 7 4 9
356 153 mul02i ⊢ ( 0 · 7 ) = 0
357 28 29 3 184 355 356 decmul1 ⊢ ( 1 0 7 0 · 7 ) = 7 4 9 0
358 30 10 28 186 3 327 351 357 decmul2c ⊢ ( 1 0 7 0 · 1 0 7 ) = 1 1 4 4 9 0
359 325 3 3 358 61 decaddi ⊢ ( ( 1 0 7 0 · 1 0 7 ) + 0 ) = 1 1 4 4 9 0
360 348 62 eqtri ⊢ ( 1 0 7 0 · 0 ) = 0 0
361 30 29 3 184 3 3 359 360 decmul2c ⊢ ( 1 0 7 0 · 1 0 7 0 ) = 1 1 4 4 9 0 0
362 321 361 eqtr4i ⊢ ( ( 2 8 6 · 𝑁 ) + 6 1 4 ) = ( 1 0 7 0 · 1 0 7 0 )
363 8 9 23 27 30 18 280 284 362 mod2xi ⊢ ( ( 2 ↑ 1 0 0 ) mod 𝑁 ) = ( 6 1 4 mod 𝑁 )
364 11 nn0cni ⊢ 1 0 0 ∈ ℂ
365 eqid ⊢ 1 0 0 = 1 0 0
366 20 10 3 365 173 241 decmul1 ⊢ ( 1 0 0 · 2 ) = 2 0 0
367 364 51 366 mulcomli ⊢ ( 2 · 1 0 0 ) = 2 0 0
368 eqid ⊢ 9 0 2 = 9 0 2
369 eqid ⊢ 9 0 = 9 0
370 12 3 12 369 75 decaddi ⊢ ( 9 0 + 9 ) = 9 9
371 eqid ⊢ 9 4 = 9 4
372 6p1e7 ⊢ ( 6 + 1 ) = 7
373 9t4e36 ⊢ ( 9 · 4 ) = 3 6
374 41 15 372 373 decsuc ⊢ ( ( 9 · 4 ) + 1 ) = 3 7
375 103 61 oveq12i ⊢ ( ( 4 · 4 ) + ( 0 + 0 ) ) = ( 1 6 + 0 )
376 16 15 deccl ⊢ 1 6 ∈ ℕ0
377 376 nn0cni ⊢ 1 6 ∈ ℂ
378 377 addridi ⊢ ( 1 6 + 0 ) = 1 6
379 375 378 eqtri ⊢ ( ( 4 · 4 ) + ( 0 + 0 ) ) = 1 6
380 12 2 292 371 2 15 16 374 379 decrmac ⊢ ( ( 9 4 · 4 ) + ( 0 + 0 ) ) = 3 7 6
381 238 mul01i ⊢ ( 9 4 · 0 ) = 0
382 381 oveq1i ⊢ ( ( 9 4 · 0 ) + 9 ) = ( 0 + 9 )
383 382 75 58 3eqtri ⊢ ( ( 9 4 · 0 ) + 9 ) = 0 9
384 2 3 3 12 60 59 13 12 3 380 383 decma2c ⊢ ( ( 9 4 · 4 0 ) + ( 9 + 0 ) ) = 3 7 6 9
385 4 3 12 12 55 370 13 12 3 384 383 decma2c ⊢ ( ( 9 4 · 4 0 0 ) + ( 9 0 + 9 ) ) = 3 7 6 9 9
386 56 mulridi ⊢ ( 9 · 1 ) = 9
387 64 mulridi ⊢ ( 4 · 1 ) = 4
388 387 oveq1i ⊢ ( ( 4 · 1 ) + 2 ) = ( 4 + 2 )
389 388 203 eqtri ⊢ ( ( 4 · 1 ) + 2 ) = 6
390 12 2 20 371 16 386 389 decrmanc ⊢ ( ( 9 4 · 1 ) + 2 ) = 9 6
391 5 16 19 20 1 368 13 15 12 385 390 decma2c ⊢ ( ( 9 4 · 𝑁 ) + 9 0 2 ) = 3 7 6 9 9 6
392 38 22 deccl ⊢ 2 4 5 ∈ ℕ0
393 eqid ⊢ 2 4 5 = 2 4 5
394 50 51 199 addcomli ⊢ ( 2 + 6 ) = 8
395 20 2 15 16 165 287 394 101 decadd ⊢ ( 2 4 + 6 1 ) = 8 5
396 8p2e10 ⊢ ( 8 + 2 ) = 1 0
397 41 15 372 90 decsuc ⊢ ( ( 6 · 6 ) + 1 ) = 3 7
398 50 mullidi ⊢ ( 1 · 6 ) = 6
399 398 oveq1i ⊢ ( ( 1 · 6 ) + 0 ) = ( 6 + 0 )
400 50 addridi ⊢ ( 6 + 0 ) = 6
401 399 400 eqtri ⊢ ( ( 1 · 6 ) + 0 ) = 6
402 15 16 16 3 287 396 15 397 401 decma ⊢ ( ( 6 1 · 6 ) + ( 8 + 2 ) ) = 3 7 6
403 17 2 24 22 285 395 15 12 20 402 99 decmac ⊢ ( ( 6 1 4 · 6 ) + ( 2 4 + 6 1 ) ) = 3 7 6 9
404 16 15 16 287 317 78 decmul1 ⊢ ( 6 1 · 1 ) = 6 1
405 387 oveq1i ⊢ ( ( 4 · 1 ) + 5 ) = ( 4 + 5 )
406 405 98 eqtri ⊢ ( ( 4 · 1 ) + 5 ) = 9
407 17 2 22 285 16 404 406 decrmanc ⊢ ( ( 6 1 4 · 1 ) + 5 ) = 6 1 9
408 15 16 38 22 287 393 18 12 17 403 407 decma2c ⊢ ( ( 6 1 4 · 6 1 ) + 2 4 5 ) = 3 7 6 9 9
409 65 oveq1i ⊢ ( ( 1 · 4 ) + 1 ) = ( 4 + 1 )
410 409 101 eqtri ⊢ ( ( 1 · 4 ) + 1 ) = 5
411 15 16 16 287 2 95 410 decrmanc ⊢ ( ( 6 1 · 4 ) + 1 ) = 2 4 5
412 2 17 2 285 15 16 411 103 decmul1c ⊢ ( 6 1 4 · 4 ) = 2 4 5 6
413 18 17 2 285 15 392 408 412 decmul2c ⊢ ( 6 1 4 · 6 1 4 ) = 3 7 6 9 9 6
414 391 413 eqtr4i ⊢ ( ( 9 4 · 𝑁 ) + 9 0 2 ) = ( 6 1 4 · 6 1 4 )
415 8 9 11 14 18 21 363 367 414 mod2xi ⊢ ( ( 2 ↑ 2 0 0 ) mod 𝑁 ) = ( 9 0 2 mod 𝑁 )