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