Metamath Proof Explorer

Theorem 4001lem2

Description: Lemma for 4001prm . Calculate a power mod. In decimal, we calculate 2 ^ 4 0 0 = ( 2 ^ 2 0 0 ) ^ 2 == 9 0 2 ^ 2 = 2 0 3 N + 1 4 0 1 and 2 ^ 8 0 0 = ( 2 ^ 4 0 0 ) ^ 2 == 1 4 0 1 ^ 2 = 4 9 0 N + 2 3 1 1 == 2 3 1 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 4001prm.1 ⊢ 𝑁 = 4 0 0 1
Assertion 4001lem2 ( ( 2 ↑ 8 0 0 ) mod 𝑁 ) = ( 2 3 1 1 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 9nn0 ⊢ 9 ∈ ℕ0
11 2 10 deccl ⊢ 4 9 ∈ ℕ0
12 11 3 deccl ⊢ 4 9 0 ∈ ℕ0
13 12 nn0zi ⊢ 4 9 0 ∈ ℤ
14 1nn0 ⊢ 1 ∈ ℕ0
15 14 2 deccl ⊢ 1 4 ∈ ℕ0
16 15 3 deccl ⊢ 1 4 0 ∈ ℕ0
17 16 14 deccl ⊢ 1 4 0 1 ∈ ℕ0
18 2nn0 ⊢ 2 ∈ ℕ0
19 3nn0 ⊢ 3 ∈ ℕ0
20 18 19 deccl ⊢ 2 3 ∈ ℕ0
21 20 14 deccl ⊢ 2 3 1 ∈ ℕ0
22 21 14 deccl ⊢ 2 3 1 1 ∈ ℕ0
23 18 3 deccl ⊢ 2 0 ∈ ℕ0
24 23 3 deccl ⊢ 2 0 0 ∈ ℕ0
25 23 19 deccl ⊢ 2 0 3 ∈ ℕ0
26 25 nn0zi ⊢ 2 0 3 ∈ ℤ
27 10 3 deccl ⊢ 9 0 ∈ ℕ0
28 27 18 deccl ⊢ 9 0 2 ∈ ℕ0
29 1 4001lem1 ⊢ ( ( 2 ↑ 2 0 0 ) mod 𝑁 ) = ( 9 0 2 mod 𝑁 )
30 24 nn0cni ⊢ 2 0 0 ∈ ℂ
31 2cn ⊢ 2 ∈ ℂ
32 eqid ⊢ 2 0 0 = 2 0 0
33 eqid ⊢ 2 0 = 2 0
34 2t2e4 ⊢ ( 2 · 2 ) = 4
35 31 mul02i ⊢ ( 0 · 2 ) = 0
36 18 18 3 33 34 35 decmul1 ⊢ ( 2 0 · 2 ) = 4 0
37 18 23 3 32 36 35 decmul1 ⊢ ( 2 0 0 · 2 ) = 4 0 0
38 30 31 37 mulcomli ⊢ ( 2 · 2 0 0 ) = 4 0 0
39 eqid ⊢ 1 4 0 1 = 1 4 0 1
40 6nn0 ⊢ 6 ∈ ℕ0
41 14 40 deccl ⊢ 1 6 ∈ ℕ0
42 eqid ⊢ 4 0 0 = 4 0 0
43 eqid ⊢ 1 4 0 = 1 4 0
44 eqid ⊢ 1 4 = 1 4
45 4p2e6 ⊢ ( 4 + 2 ) = 6
46 14 2 18 44 45 decaddi ⊢ ( 1 4 + 2 ) = 1 6
47 00id ⊢ ( 0 + 0 ) = 0
48 15 3 18 3 43 33 46 47 decadd ⊢ ( 1 4 0 + 2 0 ) = 1 6 0
49 eqid ⊢ 4 0 = 4 0
50 41 nn0cni ⊢ 1 6 ∈ ℂ
51 50 addid1i ⊢ ( 1 6 + 0 ) = 1 6
52 eqid ⊢ 2 0 3 = 2 0 3
53 ax-1cn ⊢ 1 ∈ ℂ
54 53 addid1i ⊢ ( 1 + 0 ) = 1
55 14 dec0h ⊢ 1 = 0 1
56 54 55 eqtri ⊢ ( 1 + 0 ) = 0 1
57 53 addid2i ⊢ ( 0 + 1 ) = 1
58 57 14 eqeltri ⊢ ( 0 + 1 ) ∈ ℕ0
59 4cn ⊢ 4 ∈ ℂ
60 4t2e8 ⊢ ( 4 · 2 ) = 8
61 59 31 60 mulcomli ⊢ ( 2 · 4 ) = 8
62 59 mul02i ⊢ ( 0 · 4 ) = 0
63 62 57 oveq12i ⊢ ( ( 0 · 4 ) + ( 0 + 1 ) ) = ( 0 + 1 )
64 63 57 eqtri ⊢ ( ( 0 · 4 ) + ( 0 + 1 ) ) = 1
65 18 3 58 33 2 61 64 decrmanc ⊢ ( ( 2 0 · 4 ) + ( 0 + 1 ) ) = 8 1
66 2p1e3 ⊢ ( 2 + 1 ) = 3
67 3cn ⊢ 3 ∈ ℂ
68 4t3e12 ⊢ ( 4 · 3 ) = 1 2
69 59 67 68 mulcomli ⊢ ( 3 · 4 ) = 1 2
70 14 18 66 69 decsuc ⊢ ( ( 3 · 4 ) + 1 ) = 1 3
71 23 19 3 14 52 56 2 19 14 65 70 decmac ⊢ ( ( 2 0 3 · 4 ) + ( 1 + 0 ) ) = 8 1 3
72 25 nn0cni ⊢ 2 0 3 ∈ ℂ
73 72 mul01i ⊢ ( 2 0 3 · 0 ) = 0
74 73 oveq1i ⊢ ( ( 2 0 3 · 0 ) + 6 ) = ( 0 + 6 )
75 6cn ⊢ 6 ∈ ℂ
76 75 addid2i ⊢ ( 0 + 6 ) = 6
77 40 dec0h ⊢ 6 = 0 6
78 74 76 77 3eqtri ⊢ ( ( 2 0 3 · 0 ) + 6 ) = 0 6
79 2 3 14 40 49 51 25 40 3 71 78 decma2c ⊢ ( ( 2 0 3 · 4 0 ) + ( 1 6 + 0 ) ) = 8 1 3 6
80 73 oveq1i ⊢ ( ( 2 0 3 · 0 ) + 0 ) = ( 0 + 0 )
81 3 dec0h ⊢ 0 = 0 0
82 80 47 81 3eqtri ⊢ ( ( 2 0 3 · 0 ) + 0 ) = 0 0
83 4 3 41 3 42 48 25 3 3 79 82 decma2c ⊢ ( ( 2 0 3 · 4 0 0 ) + ( 1 4 0 + 2 0 ) ) = 8 1 3 6 0
84 31 mulid1i ⊢ ( 2 · 1 ) = 2
85 53 mul02i ⊢ ( 0 · 1 ) = 0
86 14 18 3 33 84 85 decmul1 ⊢ ( 2 0 · 1 ) = 2 0
87 67 mulid1i ⊢ ( 3 · 1 ) = 3
88 87 oveq1i ⊢ ( ( 3 · 1 ) + 1 ) = ( 3 + 1 )
89 3p1e4 ⊢ ( 3 + 1 ) = 4
90 88 89 eqtri ⊢ ( ( 3 · 1 ) + 1 ) = 4
91 23 19 14 52 14 86 90 decrmanc ⊢ ( ( 2 0 3 · 1 ) + 1 ) = 2 0 4
92 5 14 16 14 1 39 25 2 23 83 91 decma2c ⊢ ( ( 2 0 3 · 𝑁 ) + 1 4 0 1 ) = 8 1 3 6 0 4
93 eqid ⊢ 9 0 2 = 9 0 2
94 8nn0 ⊢ 8 ∈ ℕ0
95 14 94 deccl ⊢ 1 8 ∈ ℕ0
96 95 3 deccl ⊢ 1 8 0 ∈ ℕ0
97 eqid ⊢ 9 0 = 9 0
98 eqid ⊢ 1 8 0 = 1 8 0
99 95 nn0cni ⊢ 1 8 ∈ ℂ
100 99 addid1i ⊢ ( 1 8 + 0 ) = 1 8
101 1p2e3 ⊢ ( 1 + 2 ) = 3
102 101 19 eqeltri ⊢ ( 1 + 2 ) ∈ ℕ0
103 9t9e81 ⊢ ( 9 · 9 ) = 8 1
104 9cn ⊢ 9 ∈ ℂ
105 104 mul02i ⊢ ( 0 · 9 ) = 0
106 105 101 oveq12i ⊢ ( ( 0 · 9 ) + ( 1 + 2 ) ) = ( 0 + 3 )
107 67 addid2i ⊢ ( 0 + 3 ) = 3
108 106 107 eqtri ⊢ ( ( 0 · 9 ) + ( 1 + 2 ) ) = 3
109 10 3 102 97 10 103 108 decrmanc ⊢ ( ( 9 0 · 9 ) + ( 1 + 2 ) ) = 8 1 3
110 9t2e18 ⊢ ( 9 · 2 ) = 1 8
111 104 31 110 mulcomli ⊢ ( 2 · 9 ) = 1 8
112 1p1e2 ⊢ ( 1 + 1 ) = 2
113 8p8e16 ⊢ ( 8 + 8 ) = 1 6
114 14 94 94 111 112 40 113 decaddci ⊢ ( ( 2 · 9 ) + 8 ) = 2 6
115 27 18 14 94 93 100 10 40 18 109 114 decmac ⊢ ( ( 9 0 2 · 9 ) + ( 1 8 + 0 ) ) = 8 1 3 6
116 28 nn0cni ⊢ 9 0 2 ∈ ℂ
117 116 mul01i ⊢ ( 9 0 2 · 0 ) = 0
118 117 oveq1i ⊢ ( ( 9 0 2 · 0 ) + 0 ) = ( 0 + 0 )
119 118 47 81 3eqtri ⊢ ( ( 9 0 2 · 0 ) + 0 ) = 0 0
120 10 3 95 3 97 98 28 3 3 115 119 decma2c ⊢ ( ( 9 0 2 · 9 0 ) + 1 8 0 ) = 8 1 3 6 0
121 18 10 3 97 110 35 decmul1 ⊢ ( 9 0 · 2 ) = 1 8 0
122 18 27 18 93 121 34 decmul1 ⊢ ( 9 0 2 · 2 ) = 1 8 0 4
123 28 27 18 93 2 96 120 122 decmul2c ⊢ ( 9 0 2 · 9 0 2 ) = 8 1 3 6 0 4
124 92 123 eqtr4i ⊢ ( ( 2 0 3 · 𝑁 ) + 1 4 0 1 ) = ( 9 0 2 · 9 0 2 )
125 8 9 24 26 28 17 29 38 124 mod2xi ⊢ ( ( 2 ↑ 4 0 0 ) mod 𝑁 ) = ( 1 4 0 1 mod 𝑁 )
126 5 nn0cni ⊢ 4 0 0 ∈ ℂ
127 18 2 3 49 60 35 decmul1 ⊢ ( 4 0 · 2 ) = 8 0
128 18 4 3 42 127 35 decmul1 ⊢ ( 4 0 0 · 2 ) = 8 0 0
129 126 31 128 mulcomli ⊢ ( 2 · 4 0 0 ) = 8 0 0
130 eqid ⊢ 2 3 1 1 = 2 3 1 1
131 18 94 deccl ⊢ 2 8 ∈ ℕ0
132 eqid ⊢ 2 3 1 = 2 3 1
133 eqid ⊢ 4 9 = 4 9
134 7nn0 ⊢ 7 ∈ ℕ0
135 7p1e8 ⊢ ( 7 + 1 ) = 8
136 eqid ⊢ 2 3 = 2 3
137 4p3e7 ⊢ ( 4 + 3 ) = 7
138 59 67 137 addcomli ⊢ ( 3 + 4 ) = 7
139 18 19 2 136 138 decaddi ⊢ ( 2 3 + 4 ) = 2 7
140 18 134 135 139 decsuc ⊢ ( ( 2 3 + 4 ) + 1 ) = 2 8
141 9p1e10 ⊢ ( 9 + 1 ) = 1 0
142 104 53 141 addcomli ⊢ ( 1 + 9 ) = 1 0
143 20 14 2 10 132 133 140 142 decaddc2 ⊢ ( 2 3 1 + 4 9 ) = 2 8 0
144 131 nn0cni ⊢ 2 8 ∈ ℂ
145 144 addid1i ⊢ ( 2 8 + 0 ) = 2 8
146 31 addid1i ⊢ ( 2 + 0 ) = 2
147 146 18 eqeltri ⊢ ( 2 + 0 ) ∈ ℕ0
148 eqid ⊢ 4 9 0 = 4 9 0
149 4t4e16 ⊢ ( 4 · 4 ) = 1 6
150 6p3e9 ⊢ ( 6 + 3 ) = 9
151 14 40 19 149 150 decaddi ⊢ ( ( 4 · 4 ) + 3 ) = 1 9
152 9t4e36 ⊢ ( 9 · 4 ) = 3 6
153 2 2 10 133 40 19 151 152 decmul1c ⊢ ( 4 9 · 4 ) = 1 9 6
154 62 146 oveq12i ⊢ ( ( 0 · 4 ) + ( 2 + 0 ) ) = ( 0 + 2 )
155 31 addid2i ⊢ ( 0 + 2 ) = 2
156 154 155 eqtri ⊢ ( ( 0 · 4 ) + ( 2 + 0 ) ) = 2
157 11 3 147 148 2 153 156 decrmanc ⊢ ( ( 4 9 0 · 4 ) + ( 2 + 0 ) ) = 1 9 6 2
158 12 nn0cni ⊢ 4 9 0 ∈ ℂ
159 158 mul01i ⊢ ( 4 9 0 · 0 ) = 0
160 159 oveq1i ⊢ ( ( 4 9 0 · 0 ) + 8 ) = ( 0 + 8 )
161 8cn ⊢ 8 ∈ ℂ
162 161 addid2i ⊢ ( 0 + 8 ) = 8
163 94 dec0h ⊢ 8 = 0 8
164 160 162 163 3eqtri ⊢ ( ( 4 9 0 · 0 ) + 8 ) = 0 8
165 2 3 18 94 49 145 12 94 3 157 164 decma2c ⊢ ( ( 4 9 0 · 4 0 ) + ( 2 8 + 0 ) ) = 1 9 6 2 8
166 159 oveq1i ⊢ ( ( 4 9 0 · 0 ) + 0 ) = ( 0 + 0 )
167 166 47 81 3eqtri ⊢ ( ( 4 9 0 · 0 ) + 0 ) = 0 0
168 4 3 131 3 42 143 12 3 3 165 167 decma2c ⊢ ( ( 4 9 0 · 4 0 0 ) + ( 2 3 1 + 4 9 ) ) = 1 9 6 2 8 0
169 59 mulid1i ⊢ ( 4 · 1 ) = 4
170 104 mulid1i ⊢ ( 9 · 1 ) = 9
171 14 2 10 133 169 170 decmul1 ⊢ ( 4 9 · 1 ) = 4 9
172 85 oveq1i ⊢ ( ( 0 · 1 ) + 1 ) = ( 0 + 1 )
173 172 57 eqtri ⊢ ( ( 0 · 1 ) + 1 ) = 1
174 11 3 14 148 14 171 173 decrmanc ⊢ ( ( 4 9 0 · 1 ) + 1 ) = 4 9 1
175 5 14 21 14 1 130 12 14 11 168 174 decma2c ⊢ ( ( 4 9 0 · 𝑁 ) + 2 3 1 1 ) = 1 9 6 2 8 0 1
176 15 nn0cni ⊢ 1 4 ∈ ℂ
177 176 addid1i ⊢ ( 1 4 + 0 ) = 1 4
178 5nn0 ⊢ 5 ∈ ℕ0
179 178 40 deccl ⊢ 5 6 ∈ ℕ0
180 179 3 deccl ⊢ 5 6 0 ∈ ℕ0
181 eqid ⊢ 5 6 0 = 5 6 0
182 179 nn0cni ⊢ 5 6 ∈ ℂ
183 182 addid2i ⊢ ( 0 + 5 6 ) = 5 6
184 3 14 179 3 55 181 183 54 decadd ⊢ ( 1 + 5 6 0 ) = 5 6 1
185 182 addid1i ⊢ ( 5 6 + 0 ) = 5 6
186 5cn ⊢ 5 ∈ ℂ
187 186 addid1i ⊢ ( 5 + 0 ) = 5
188 187 178 eqeltri ⊢ ( 5 + 0 ) ∈ ℕ0
189 53 mulid1i ⊢ ( 1 · 1 ) = 1
190 169 187 oveq12i ⊢ ( ( 4 · 1 ) + ( 5 + 0 ) ) = ( 4 + 5 )
191 5p4e9 ⊢ ( 5 + 4 ) = 9
192 186 59 191 addcomli ⊢ ( 4 + 5 ) = 9
193 190 192 eqtri ⊢ ( ( 4 · 1 ) + ( 5 + 0 ) ) = 9
194 14 2 188 44 14 189 193 decrmanc ⊢ ( ( 1 4 · 1 ) + ( 5 + 0 ) ) = 1 9
195 85 oveq1i ⊢ ( ( 0 · 1 ) + 6 ) = ( 0 + 6 )
196 195 76 77 3eqtri ⊢ ( ( 0 · 1 ) + 6 ) = 0 6
197 15 3 178 40 43 185 14 40 3 194 196 decmac ⊢ ( ( 1 4 0 · 1 ) + ( 5 6 + 0 ) ) = 1 9 6
198 189 oveq1i ⊢ ( ( 1 · 1 ) + 1 ) = ( 1 + 1 )
199 18 dec0h ⊢ 2 = 0 2
200 198 112 199 3eqtri ⊢ ( ( 1 · 1 ) + 1 ) = 0 2
201 16 14 179 14 39 184 14 18 3 197 200 decmac ⊢ ( ( 1 4 0 1 · 1 ) + ( 1 + 5 6 0 ) ) = 1 9 6 2
202 59 mulid2i ⊢ ( 1 · 4 ) = 4
203 202 oveq1i ⊢ ( ( 1 · 4 ) + 1 ) = ( 4 + 1 )
204 4p1e5 ⊢ ( 4 + 1 ) = 5
205 203 204 eqtri ⊢ ( ( 1 · 4 ) + 1 ) = 5
206 2 14 2 44 40 14 205 149 decmul1c ⊢ ( 1 4 · 4 ) = 5 6
207 75 addid1i ⊢ ( 6 + 0 ) = 6
208 178 40 3 206 207 decaddi ⊢ ( ( 1 4 · 4 ) + 0 ) = 5 6
209 0cn ⊢ 0 ∈ ℂ
210 59 mul01i ⊢ ( 4 · 0 ) = 0
211 210 81 eqtri ⊢ ( 4 · 0 ) = 0 0
212 59 209 211 mulcomli ⊢ ( 0 · 4 ) = 0 0
213 2 15 3 43 3 3 208 212 decmul1c ⊢ ( 1 4 0 · 4 ) = 5 6 0
214 202 oveq1i ⊢ ( ( 1 · 4 ) + 4 ) = ( 4 + 4 )
215 4p4e8 ⊢ ( 4 + 4 ) = 8
216 214 215 eqtri ⊢ ( ( 1 · 4 ) + 4 ) = 8
217 16 14 2 39 2 213 216 decrmanc ⊢ ( ( 1 4 0 1 · 4 ) + 4 ) = 5 6 0 8
218 14 2 14 2 44 177 17 94 180 201 217 decma2c ⊢ ( ( 1 4 0 1 · 1 4 ) + ( 1 4 + 0 ) ) = 1 9 6 2 8
219 17 nn0cni ⊢ 1 4 0 1 ∈ ℂ
220 219 mul01i ⊢ ( 1 4 0 1 · 0 ) = 0
221 220 oveq1i ⊢ ( ( 1 4 0 1 · 0 ) + 0 ) = ( 0 + 0 )
222 221 47 81 3eqtri ⊢ ( ( 1 4 0 1 · 0 ) + 0 ) = 0 0
223 15 3 15 3 43 43 17 3 3 218 222 decma2c ⊢ ( ( 1 4 0 1 · 1 4 0 ) + 1 4 0 ) = 1 9 6 2 8 0
224 219 mulid1i ⊢ ( 1 4 0 1 · 1 ) = 1 4 0 1
225 17 16 14 39 14 16 223 224 decmul2c ⊢ ( 1 4 0 1 · 1 4 0 1 ) = 1 9 6 2 8 0 1
226 175 225 eqtr4i ⊢ ( ( 4 9 0 · 𝑁 ) + 2 3 1 1 ) = ( 1 4 0 1 · 1 4 0 1 )
227 8 9 5 13 17 22 125 129 226 mod2xi ⊢ ( ( 2 ↑ 8 0 0 ) mod 𝑁 ) = ( 2 3 1 1 mod 𝑁 )