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 2t4e8 ⊢ ( 2 · 4 ) = 8
122 69 addridi ⊢ ( 1 + 0 ) = 1
123 121 122 oveq12i ⊢ ( ( 2 · 4 ) + ( 1 + 0 ) ) = ( 8 + 1 )
124 8p1e9 ⊢ ( 8 + 1 ) = 9
125 123 124 eqtri ⊢ ( ( 2 · 4 ) + ( 1 + 0 ) ) = 9
126 51 mul01i ⊢ ( 2 · 0 ) = 0
127 126 oveq1i ⊢ ( ( 2 · 0 ) + 0 ) = ( 0 + 0 )
128 127 61 62 3eqtri ⊢ ( ( 2 · 0 ) + 0 ) = 0 0
129 2 3 16 3 60 120 20 3 3 125 128 decma2c ⊢ ( ( 2 · 4 0 ) + ( 1 0 + 0 ) ) = 9 0
130 126 oveq1i ⊢ ( ( 2 · 0 ) + 2 ) = ( 0 + 2 )
131 51 addlidi ⊢ ( 0 + 2 ) = 2
132 20 dec0h ⊢ 2 = 0 2
133 130 131 132 3eqtri ⊢ ( ( 2 · 0 ) + 2 ) = 0 2
134 4 3 10 20 55 119 20 20 3 129 133 decma2c ⊢ ( ( 2 · 4 0 0 ) + ( 1 0 2 + 0 ) ) = 9 0 2
135 109 oveq1i ⊢ ( ( 2 · 1 ) + 3 ) = ( 2 + 3 )
136 3cn ⊢ 3 ∈ ℂ
137 3p2e5 ⊢ ( 3 + 2 ) = 5
138 136 51 137 addcomli ⊢ ( 2 + 3 ) = 5
139 22 dec0h ⊢ 5 = 0 5
140 135 138 139 3eqtri ⊢ ( ( 2 · 1 ) + 3 ) = 0 5
141 5 16 40 41 1 117 20 22 3 134 140 decma2c ⊢ ( ( 2 · 𝑁 ) + 1 0 2 3 ) = 9 0 2 5
142 2 28 deccl ⊢ 4 7 ∈ ℕ0
143 eqid ⊢ 4 7 = 4 7
144 98 oveq2i ⊢ ( ( 9 · 9 ) + ( 4 + 5 ) ) = ( ( 9 · 9 ) + 9 )
145 9t9e81 ⊢ ( 9 · 9 ) = 8 1
146 9p1e10 ⊢ ( 9 + 1 ) = 1 0
147 56 69 146 addcomli ⊢ ( 1 + 9 ) = 1 0
148 24 16 12 145 124 147 decaddci2 ⊢ ( ( 9 · 9 ) + 9 ) = 9 0
149 144 148 eqtri ⊢ ( ( 9 · 9 ) + ( 4 + 5 ) ) = 9 0
150 9t5e45 ⊢ ( 9 · 5 ) = 4 5
151 56 80 150 mulcomli ⊢ ( 5 · 9 ) = 4 5
152 7cn ⊢ 7 ∈ ℂ
153 7p5e12 ⊢ ( 7 + 5 ) = 1 2
154 152 80 153 addcomli ⊢ ( 5 + 7 ) = 1 2
155 2 22 28 151 101 20 154 decaddci ⊢ ( ( 5 · 9 ) + 7 ) = 5 2
156 12 22 2 28 54 143 12 20 22 149 155 decmac ⊢ ( ( 9 5 · 9 ) + 4 7 ) = 9 0 2
157 5p2e7 ⊢ ( 5 + 2 ) = 7
158 2 22 20 150 157 decaddi ⊢ ( ( 9 · 5 ) + 2 ) = 4 7
159 5t5e25 ⊢ ( 5 · 5 ) = 2 5
160 22 12 22 54 22 20 158 159 decmul1c ⊢ ( 9 5 · 5 ) = 4 7 5
161 45 12 22 54 22 142 156 160 decmul2c ⊢ ( 9 5 · 9 5 ) = 9 0 2 5
162 141 161 eqtr4i ⊢ ( ( 2 · 𝑁 ) + 1 0 2 3 ) = ( 9 5 · 9 5 )
163 8 9 43 44 45 42 107 116 162 mod2xi ⊢ ( ( 2 ↑ 2 4 ) mod 𝑁 ) = ( 1 0 2 3 mod 𝑁 )
164 eqid ⊢ 2 4 = 2 4
165 20 2 101 164 decsuc ⊢ ( 2 4 + 1 ) = 2 5
166 37 nn0cni ⊢ 2 0 4 6 ∈ ℂ
167 166 addlidi ⊢ ( 0 + 2 0 4 6 ) = 2 0 4 6
168 8 nncni ⊢ 𝑁 ∈ ℂ
169 168 mul02i ⊢ ( 0 · 𝑁 ) = 0
170 169 oveq1i ⊢ ( ( 0 · 𝑁 ) + 2 0 4 6 ) = ( 0 + 2 0 4 6 )
171 eqid ⊢ 1 0 2 = 1 0 2
172 20 dec0u ⊢ ( 1 0 · 2 ) = 2 0
173 20 10 20 171 172 113 decmul1 ⊢ ( 1 0 2 · 2 ) = 2 0 4
174 3t2e6 ⊢ ( 3 · 2 ) = 6
175 20 40 41 117 173 174 decmul1 ⊢ ( 1 0 2 3 · 2 ) = 2 0 4 6
176 167 170 175 3eqtr4i ⊢ ( ( 0 · 𝑁 ) + 2 0 4 6 ) = ( 1 0 2 3 · 2 )
177 8 9 38 39 42 37 163 165 176 modxp1i ⊢ ( ( 2 ↑ 2 5 ) mod 𝑁 ) = ( 2 0 4 6 mod 𝑁 )
178 113 oveq1i ⊢ ( ( 2 · 2 ) + 1 ) = ( 4 + 1 )
179 178 101 eqtri ⊢ ( ( 2 · 2 ) + 1 ) = 5
180 5t2e10 ⊢ ( 5 · 2 ) = 1 0
181 80 51 180 mulcomli ⊢ ( 2 · 5 ) = 1 0
182 20 20 22 87 3 16 179 181 decmul2c ⊢ ( 2 · 2 5 ) = 5 0
183 eqid ⊢ 1 0 7 0 = 1 0 7 0
184 20 16 deccl ⊢ 2 1 ∈ ℕ0
185 eqid ⊢ 1 0 7 = 1 0 7
186 eqid ⊢ 1 0 4 = 1 0 4
187 0p1e1 ⊢ ( 0 + 1 ) = 1
188 10p10e20 ⊢ ( 1 0 + 1 0 ) = 2 0
189 20 3 187 188 decsuc ⊢ ( ( 1 0 + 1 0 ) + 1 ) = 2 1
190 7p4e11 ⊢ ( 7 + 4 ) = 1 1
191 10 28 10 2 185 186 189 16 190 decaddc ⊢ ( 1 0 7 + 1 0 4 ) = 2 1 1
192 184 nn0cni ⊢ 2 1 ∈ ℂ
193 192 addridi ⊢ ( 2 1 + 0 ) = 2 1
194 111 20 eqeltri ⊢ ( 2 + 0 ) ∈ ℕ0
195 eqid ⊢ 1 0 4 6 = 1 0 4 6
196 dfdec10 ⊢ 4 1 = ( ( 1 0 · 4 ) + 1 )
197 196 eqcomi ⊢ ( ( 1 0 · 4 ) + 1 ) = 4 1
198 6p2e8 ⊢ ( 6 + 2 ) = 8
199 16 15 20 103 198 decaddi ⊢ ( ( 4 · 4 ) + 2 ) = 1 8
200 10 2 20 186 2 24 16 197 199 decrmac ⊢ ( ( 1 0 4 · 4 ) + 2 ) = 4 1 8
201 95 111 oveq12i ⊢ ( ( 6 · 4 ) + ( 2 + 0 ) ) = ( 2 4 + 2 )
202 4p2e6 ⊢ ( 4 + 2 ) = 6
203 20 2 20 164 202 decaddi ⊢ ( 2 4 + 2 ) = 2 6
204 201 203 eqtri ⊢ ( ( 6 · 4 ) + ( 2 + 0 ) ) = 2 6
205 32 15 194 195 2 15 20 200 204 decrmac ⊢ ( ( 1 0 4 6 · 4 ) + ( 2 + 0 ) ) = 4 1 8 6
206 33 nn0cni ⊢ 1 0 4 6 ∈ ℂ
207 206 mul01i ⊢ ( 1 0 4 6 · 0 ) = 0
208 207 oveq1i ⊢ ( ( 1 0 4 6 · 0 ) + 1 ) = ( 0 + 1 )
209 16 dec0h ⊢ 1 = 0 1
210 208 187 209 3eqtri ⊢ ( ( 1 0 4 6 · 0 ) + 1 ) = 0 1
211 2 3 20 16 60 193 33 16 3 205 210 decma2c ⊢ ( ( 1 0 4 6 · 4 0 ) + ( 2 1 + 0 ) ) = 4 1 8 6 1
212 4 3 184 16 55 191 33 16 3 211 210 decma2c ⊢ ( ( 1 0 4 6 · 4 0 0 ) + ( 1 0 7 + 1 0 4 ) ) = 4 1 8 6 1 1
213 206 mulridi ⊢ ( 1 0 4 6 · 1 ) = 1 0 4 6
214 213 oveq1i ⊢ ( ( 1 0 4 6 · 1 ) + 0 ) = ( 1 0 4 6 + 0 )
215 206 addridi ⊢ ( 1 0 4 6 + 0 ) = 1 0 4 6
216 214 215 eqtri ⊢ ( ( 1 0 4 6 · 1 ) + 0 ) = 1 0 4 6
217 5 16 29 3 1 183 33 15 32 212 216 decma2c ⊢ ( ( 1 0 4 6 · 𝑁 ) + 1 0 7 0 ) = 4 1 8 6 1 1 6
218 eqid ⊢ 2 0 4 6 = 2 0 4 6
219 43 20 deccl ⊢ 1 2 2 ∈ ℕ0
220 219 28 deccl ⊢ 1 2 2 7 ∈ ℕ0
221 eqid ⊢ 2 0 4 = 2 0 4
222 eqid ⊢ 1 2 2 7 = 1 2 2 7
223 24 16 deccl ⊢ 8 1 ∈ ℕ0
224 223 12 deccl ⊢ 8 1 9 ∈ ℕ0
225 eqid ⊢ 2 0 = 2 0
226 eqid ⊢ 1 2 2 = 1 2 2
227 eqid ⊢ 8 1 9 = 8 1 9
228 eqid ⊢ 8 1 = 8 1
229 8cn ⊢ 8 ∈ ℂ
230 229 69 124 addcomli ⊢ ( 1 + 8 ) = 9
231 2p1e3 ⊢ ( 2 + 1 ) = 3
232 16 20 24 16 108 228 230 231 decadd ⊢ ( 1 2 + 8 1 ) = 9 3
233 12 41 91 232 decsuc ⊢ ( ( 1 2 + 8 1 ) + 1 ) = 9 4
234 9p2e11 ⊢ ( 9 + 2 ) = 1 1
235 56 51 234 addcomli ⊢ ( 2 + 9 ) = 1 1
236 43 20 223 12 226 227 233 16 235 decaddc ⊢ ( 1 2 2 + 8 1 9 ) = 9 4 1
237 13 nn0cni ⊢ 9 4 ∈ ℂ
238 237 addridi ⊢ ( 9 4 + 0 ) = 9 4
239 122 16 eqeltri ⊢ ( 1 + 0 ) ∈ ℕ0
240 51 mul02i ⊢ ( 0 · 2 ) = 0
241 240 122 oveq12i ⊢ ( ( 0 · 2 ) + ( 1 + 0 ) ) = ( 0 + 1 )
242 241 187 eqtri ⊢ ( ( 0 · 2 ) + ( 1 + 0 ) ) = 1
243 20 3 239 225 20 113 242 decrmanc ⊢ ( ( 2 0 · 2 ) + ( 1 + 0 ) ) = 4 1
244 4t2e8 ⊢ ( 4 · 2 ) = 8
245 244 oveq1i ⊢ ( ( 4 · 2 ) + 0 ) = ( 8 + 0 )
246 229 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 221 146 20 24 3 243 248 decmac ⊢ ( ( 2 0 4 · 2 ) + ( 9 + 1 ) ) = 4 1 8
250 64 51 202 addcomli ⊢ ( 2 + 4 ) = 6
251 16 20 2 52 250 decaddi ⊢ ( ( 6 · 2 ) + 4 ) = 1 6
252 36 15 12 2 218 238 20 15 16 249 251 decmac ⊢ ( ( 2 0 4 6 · 2 ) + ( 9 4 + 0 ) ) = 4 1 8 6
253 166 mul01i ⊢ ( 2 0 4 6 · 0 ) = 0
254 253 oveq1i ⊢ ( ( 2 0 4 6 · 0 ) + 1 ) = ( 0 + 1 )
255 254 187 209 3eqtri ⊢ ( ( 2 0 4 6 · 0 ) + 1 ) = 0 1
256 20 3 13 16 225 236 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 187 16 eqeltri ⊢ ( 0 + 1 ) ∈ ℕ0
259 64 mul02i ⊢ ( 0 · 4 ) = 0
260 259 187 oveq12i ⊢ ( ( 0 · 4 ) + ( 0 + 1 ) ) = ( 0 + 1 )
261 260 187 eqtri ⊢ ( ( 0 · 4 ) + ( 0 + 1 ) ) = 1
262 20 3 258 225 2 121 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 221 257 2 12 16 262 264 decmac ⊢ ( ( 2 0 4 · 4 ) + 3 ) = 8 1 9
266 152 64 190 addcomli ⊢ ( 4 + 7 ) = 1 1
267 20 2 28 95 231 16 266 decaddci ⊢ ( ( 6 · 4 ) + 7 ) = 3 1
268 36 15 28 218 2 16 41 265 267 decrmac ⊢ ( ( 2 0 4 6 · 4 ) + 7 ) = 8 1 9 1
269 35 2 219 28 221 222 37 16 224 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 131 eqtri ⊢ ( ( 0 · 6 ) + 2 ) = 2
273 20 3 20 225 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 221 15 28 20 273 275 decrmac ⊢ ( ( 2 0 4 · 6 ) + 3 ) = 1 2 2 7
277 15 36 15 218 15 41 276 90 decmul1c ⊢ ( 2 0 4 6 · 6 ) = 1 2 2 7 6
278 37 36 15 218 15 220 269 277 decmul2c ⊢ ( 2 0 4 6 · 2 0 4 6 ) = 4 1 8 6 1 1 6
279 217 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 177 182 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 180 240 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 198 oveq1i ⊢ ( ( 6 + 2 ) + 1 ) = ( 8 + 1 )
290 289 124 eqtri ⊢ ( ( 6 + 2 ) + 1 ) = 9
291 15 16 20 12 287 288 290 147 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 121 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 229 mulridi ⊢ ( 8 · 1 ) = 8
315 16 20 24 294 109 314 decmul1 ⊢ ( 2 8 · 1 ) = 2 8
316 20 24 124 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 152 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 187 335 decsuc ⊢ ( ( 1 0 · 1 ) + 1 ) = 1 1
337 152 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 185 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 183 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 185 12 2 353 354 decmul1c ⊢ ( 1 0 7 · 7 ) = 7 4 9
356 152 mul02i ⊢ ( 0 · 7 ) = 0
357 28 29 3 183 355 356 decmul1 ⊢ ( 1 0 7 0 · 7 ) = 7 4 9 0
358 30 10 28 185 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 183 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 172 240 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 237 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 202 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 198 addcomli ⊢ ( 2 + 6 ) = 8
395 20 2 15 16 164 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 𝑁 )