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 = ; ; ; 4 0 0 1
Assertion 4001lem2 
|- ( ( 2 ^ ; ; 8 0 0 ) mod N ) = ( ; ; ; 2 3 1 1 mod N )

Proof

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