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 $⊢ N = 4001$
Assertion 4001lem2 $⊢ 2 800 mod N = 2311 mod N$

Proof

Step Hyp Ref Expression
1 4001prm.1 $⊢ N = 4001$
2 4nn0 $⊢ 4 ∈ ℕ 0$
3 0nn0 $⊢ 0 ∈ ℕ 0$
4 2 3 deccl $⊢ 40 ∈ ℕ 0$
5 4 3 deccl $⊢ 400 ∈ ℕ 0$
6 1nn $⊢ 1 ∈ ℕ$
7 5 6 decnncl $⊢ 4001 ∈ ℕ$
8 1 7 eqeltri $⊢ N ∈ ℕ$
9 2nn $⊢ 2 ∈ ℕ$
10 9nn0 $⊢ 9 ∈ ℕ 0$
11 2 10 deccl $⊢ 49 ∈ ℕ 0$
12 11 3 deccl $⊢ 490 ∈ ℕ 0$
13 12 nn0zi $⊢ 490 ∈ ℤ$
14 1nn0 $⊢ 1 ∈ ℕ 0$
15 14 2 deccl $⊢ 14 ∈ ℕ 0$
16 15 3 deccl $⊢ 140 ∈ ℕ 0$
17 16 14 deccl $⊢ 1401 ∈ ℕ 0$
18 2nn0 $⊢ 2 ∈ ℕ 0$
19 3nn0 $⊢ 3 ∈ ℕ 0$
20 18 19 deccl $⊢ 23 ∈ ℕ 0$
21 20 14 deccl $⊢ 231 ∈ ℕ 0$
22 21 14 deccl $⊢ 2311 ∈ ℕ 0$
23 18 3 deccl $⊢ 20 ∈ ℕ 0$
24 23 3 deccl $⊢ 200 ∈ ℕ 0$
25 23 19 deccl $⊢ 203 ∈ ℕ 0$
26 25 nn0zi $⊢ 203 ∈ ℤ$
27 10 3 deccl $⊢ 90 ∈ ℕ 0$
28 27 18 deccl $⊢ 902 ∈ ℕ 0$
29 1 4001lem1 $⊢ 2 200 mod N = 902 mod N$
30 24 nn0cni $⊢ 200 ∈ ℂ$
31 2cn $⊢ 2 ∈ ℂ$
32 eqid $⊢ 200 = 200$
33 eqid $⊢ 20 = 20$
34 2t2e4 $⊢ 2 ⋅ 2 = 4$
35 31 mul02i $⊢ 0 ⋅ 2 = 0$
36 18 18 3 33 34 35 decmul1 $⊢ 20 ⋅ 2 = 40$
37 18 23 3 32 36 35 decmul1 $⊢ 200 ⋅ 2 = 400$
38 30 31 37 mulcomli $⊢ 2 ⋅ 200 = 400$
39 eqid $⊢ 1401 = 1401$
40 6nn0 $⊢ 6 ∈ ℕ 0$
41 14 40 deccl $⊢ 16 ∈ ℕ 0$
42 eqid $⊢ 400 = 400$
43 eqid $⊢ 140 = 140$
44 eqid $⊢ 14 = 14$
45 4p2e6 $⊢ 4 + 2 = 6$
46 14 2 18 44 45 decaddi $⊢ 14 + 2 = 16$
47 00id $⊢ 0 + 0 = 0$
48 15 3 18 3 43 33 46 47 decadd $⊢ 140 + 20 = 160$
49 eqid $⊢ 40 = 40$
50 41 nn0cni $⊢ 16 ∈ ℂ$
51 50 addid1i $⊢ 16 + 0 = 16$
52 eqid $⊢ 203 = 203$
53 ax-1cn $⊢ 1 ∈ ℂ$
54 53 addid1i $⊢ 1 + 0 = 1$
55 14 dec0h $⊢ 1 = 01$
56 54 55 eqtri $⊢ 1 + 0 = 01$
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 $⊢ 20 ⋅ 4 + 0 + 1 = 81$
66 2p1e3 $⊢ 2 + 1 = 3$
67 3cn $⊢ 3 ∈ ℂ$
68 4t3e12 $⊢ 4 ⋅ 3 = 12$
69 59 67 68 mulcomli $⊢ 3 ⋅ 4 = 12$
70 14 18 66 69 decsuc $⊢ 3 ⋅ 4 + 1 = 13$
71 23 19 3 14 52 56 2 19 14 65 70 decmac $⊢ 203 ⋅ 4 + 1 + 0 = 813$
72 25 nn0cni $⊢ 203 ∈ ℂ$
73 72 mul01i $⊢ 203 ⋅ 0 = 0$
74 73 oveq1i $⊢ 203 ⋅ 0 + 6 = 0 + 6$
75 6cn $⊢ 6 ∈ ℂ$
76 75 addid2i $⊢ 0 + 6 = 6$
77 40 dec0h $⊢ 6 = 06$
78 74 76 77 3eqtri $⊢ 203 ⋅ 0 + 6 = 06$
79 2 3 14 40 49 51 25 40 3 71 78 decma2c $⊢ 203 ⋅ 40 + 16 + 0 = 8136$
80 73 oveq1i $⊢ 203 ⋅ 0 + 0 = 0 + 0$
81 3 dec0h $⊢ 0 = 00$
82 80 47 81 3eqtri $⊢ 203 ⋅ 0 + 0 = 00$
83 4 3 41 3 42 48 25 3 3 79 82 decma2c $⊢ 203 ⋅ 400 + 140 + 20 = 81360$
84 31 mulid1i $⊢ 2 ⋅ 1 = 2$
85 53 mul02i $⊢ 0 ⋅ 1 = 0$
86 14 18 3 33 84 85 decmul1 $⊢ 20 ⋅ 1 = 20$
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 $⊢ 203 ⋅ 1 + 1 = 204$
92 5 14 16 14 1 39 25 2 23 83 91 decma2c $⊢ 203 ⋅ N + 1401 = 813604$
93 eqid $⊢ 902 = 902$
94 8nn0 $⊢ 8 ∈ ℕ 0$
95 14 94 deccl $⊢ 18 ∈ ℕ 0$
96 95 3 deccl $⊢ 180 ∈ ℕ 0$
97 eqid $⊢ 90 = 90$
98 eqid $⊢ 180 = 180$
99 95 nn0cni $⊢ 18 ∈ ℂ$
100 99 addid1i $⊢ 18 + 0 = 18$
101 1p2e3 $⊢ 1 + 2 = 3$
102 101 19 eqeltri $⊢ 1 + 2 ∈ ℕ 0$
103 9t9e81 $⊢ 9 ⋅ 9 = 81$
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 $⊢ 90 ⋅ 9 + 1 + 2 = 813$
110 9t2e18 $⊢ 9 ⋅ 2 = 18$
111 104 31 110 mulcomli $⊢ 2 ⋅ 9 = 18$
112 1p1e2 $⊢ 1 + 1 = 2$
113 8p8e16 $⊢ 8 + 8 = 16$
114 14 94 94 111 112 40 113 decaddci $⊢ 2 ⋅ 9 + 8 = 26$
115 27 18 14 94 93 100 10 40 18 109 114 decmac $⊢ 902 ⋅ 9 + 18 + 0 = 8136$
116 28 nn0cni $⊢ 902 ∈ ℂ$
117 116 mul01i $⊢ 902 ⋅ 0 = 0$
118 117 oveq1i $⊢ 902 ⋅ 0 + 0 = 0 + 0$
119 118 47 81 3eqtri $⊢ 902 ⋅ 0 + 0 = 00$
120 10 3 95 3 97 98 28 3 3 115 119 decma2c $⊢ 902 ⋅ 90 + 180 = 81360$
121 18 10 3 97 110 35 decmul1 $⊢ 90 ⋅ 2 = 180$
122 18 27 18 93 121 34 decmul1 $⊢ 902 ⋅ 2 = 1804$
123 28 27 18 93 2 96 120 122 decmul2c $⊢ 902 ⋅ 902 = 813604$
124 92 123 eqtr4i $⊢ 203 ⋅ N + 1401 = 902 ⋅ 902$
125 8 9 24 26 28 17 29 38 124 mod2xi $⊢ 2 400 mod N = 1401 mod N$
126 5 nn0cni $⊢ 400 ∈ ℂ$
127 18 2 3 49 60 35 decmul1 $⊢ 40 ⋅ 2 = 80$
128 18 4 3 42 127 35 decmul1 $⊢ 400 ⋅ 2 = 800$
129 126 31 128 mulcomli $⊢ 2 ⋅ 400 = 800$
130 eqid $⊢ 2311 = 2311$
131 18 94 deccl $⊢ 28 ∈ ℕ 0$
132 eqid $⊢ 231 = 231$
133 eqid $⊢ 49 = 49$
134 7nn0 $⊢ 7 ∈ ℕ 0$
135 7p1e8 $⊢ 7 + 1 = 8$
136 eqid $⊢ 23 = 23$
137 4p3e7 $⊢ 4 + 3 = 7$
138 59 67 137 addcomli $⊢ 3 + 4 = 7$
139 18 19 2 136 138 decaddi $⊢ 23 + 4 = 27$
140 18 134 135 139 decsuc $⊢ 23 + 4 + 1 = 28$
141 9p1e10 $⊢ 9 + 1 = 10$
142 104 53 141 addcomli $⊢ 1 + 9 = 10$
143 20 14 2 10 132 133 140 142 decaddc2 $⊢ 231 + 49 = 280$
144 131 nn0cni $⊢ 28 ∈ ℂ$
145 144 addid1i $⊢ 28 + 0 = 28$
146 31 addid1i $⊢ 2 + 0 = 2$
147 146 18 eqeltri $⊢ 2 + 0 ∈ ℕ 0$
148 eqid $⊢ 490 = 490$
149 4t4e16 $⊢ 4 ⋅ 4 = 16$
150 6p3e9 $⊢ 6 + 3 = 9$
151 14 40 19 149 150 decaddi $⊢ 4 ⋅ 4 + 3 = 19$
152 9t4e36 $⊢ 9 ⋅ 4 = 36$
153 2 2 10 133 40 19 151 152 decmul1c $⊢ 49 ⋅ 4 = 196$
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 $⊢ 490 ⋅ 4 + 2 + 0 = 1962$
158 12 nn0cni $⊢ 490 ∈ ℂ$
159 158 mul01i $⊢ 490 ⋅ 0 = 0$
160 159 oveq1i $⊢ 490 ⋅ 0 + 8 = 0 + 8$
161 8cn $⊢ 8 ∈ ℂ$
162 161 addid2i $⊢ 0 + 8 = 8$
163 94 dec0h $⊢ 8 = 08$
164 160 162 163 3eqtri $⊢ 490 ⋅ 0 + 8 = 08$
165 2 3 18 94 49 145 12 94 3 157 164 decma2c $⊢ 490 ⋅ 40 + 28 + 0 = 19628$
166 159 oveq1i $⊢ 490 ⋅ 0 + 0 = 0 + 0$
167 166 47 81 3eqtri $⊢ 490 ⋅ 0 + 0 = 00$
168 4 3 131 3 42 143 12 3 3 165 167 decma2c $⊢ 490 ⋅ 400 + 231 + 49 = 196280$
169 59 mulid1i $⊢ 4 ⋅ 1 = 4$
170 104 mulid1i $⊢ 9 ⋅ 1 = 9$
171 14 2 10 133 169 170 decmul1 $⊢ 49 ⋅ 1 = 49$
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 $⊢ 490 ⋅ 1 + 1 = 491$
175 5 14 21 14 1 130 12 14 11 168 174 decma2c $⊢ 490 ⋅ N + 2311 = 1962801$
176 15 nn0cni $⊢ 14 ∈ ℂ$
177 176 addid1i $⊢ 14 + 0 = 14$
178 5nn0 $⊢ 5 ∈ ℕ 0$
179 178 40 deccl $⊢ 56 ∈ ℕ 0$
180 179 3 deccl $⊢ 560 ∈ ℕ 0$
181 eqid $⊢ 560 = 560$
182 179 nn0cni $⊢ 56 ∈ ℂ$
183 182 addid2i $⊢ 0 + 56 = 56$
184 3 14 179 3 55 181 183 54 decadd $⊢ 1 + 560 = 561$
185 182 addid1i $⊢ 56 + 0 = 56$
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 $⊢ 14 ⋅ 1 + 5 + 0 = 19$
195 85 oveq1i $⊢ 0 ⋅ 1 + 6 = 0 + 6$
196 195 76 77 3eqtri $⊢ 0 ⋅ 1 + 6 = 06$
197 15 3 178 40 43 185 14 40 3 194 196 decmac $⊢ 140 ⋅ 1 + 56 + 0 = 196$
198 189 oveq1i $⊢ 1 ⋅ 1 + 1 = 1 + 1$
199 18 dec0h $⊢ 2 = 02$
200 198 112 199 3eqtri $⊢ 1 ⋅ 1 + 1 = 02$
201 16 14 179 14 39 184 14 18 3 197 200 decmac $⊢ 1401 ⋅ 1 + 1 + 560 = 1962$
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 $⊢ 14 ⋅ 4 = 56$
207 75 addid1i $⊢ 6 + 0 = 6$
208 178 40 3 206 207 decaddi $⊢ 14 ⋅ 4 + 0 = 56$
209 0cn $⊢ 0 ∈ ℂ$
210 59 mul01i $⊢ 4 ⋅ 0 = 0$
211 210 81 eqtri $⊢ 4 ⋅ 0 = 00$
212 59 209 211 mulcomli $⊢ 0 ⋅ 4 = 00$
213 2 15 3 43 3 3 208 212 decmul1c $⊢ 140 ⋅ 4 = 560$
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 $⊢ 1401 ⋅ 4 + 4 = 5608$
218 14 2 14 2 44 177 17 94 180 201 217 decma2c $⊢ 1401 ⋅ 14 + 14 + 0 = 19628$
219 17 nn0cni $⊢ 1401 ∈ ℂ$
220 219 mul01i $⊢ 1401 ⋅ 0 = 0$
221 220 oveq1i $⊢ 1401 ⋅ 0 + 0 = 0 + 0$
222 221 47 81 3eqtri $⊢ 1401 ⋅ 0 + 0 = 00$
223 15 3 15 3 43 43 17 3 3 218 222 decma2c $⊢ 1401 ⋅ 140 + 140 = 196280$
224 219 mulid1i $⊢ 1401 ⋅ 1 = 1401$
225 17 16 14 39 14 16 223 224 decmul2c $⊢ 1401 ⋅ 1401 = 1962801$
226 175 225 eqtr4i $⊢ 490 ⋅ N + 2311 = 1401 ⋅ 1401$
227 8 9 5 13 17 22 125 129 226 mod2xi $⊢ 2 800 mod N = 2311 mod N$