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