Metamath Proof Explorer

Theorem 4001lem4

Description: Lemma for 4001prm . Calculate the GCD of 2 ^ 8 0 0 - 1 == 2 3 1 0 with N = 4 0 0 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 4001lem4 
|- ( ( ( 2 ^ ; ; 8 0 0 ) - 1 ) gcd N ) = 1

Proof

Step Hyp Ref Expression
1 4001prm.1 
 |-  N = ; ; ; 4 0 0 1
2 2nn 
 |-  2 e. NN
3 8nn0 
 |-  8 e. NN0
4 0nn0 
 |-  0 e. NN0
5 3 4 deccl 
 |-  ; 8 0 e. NN0
6 5 4 deccl 
 |-  ; ; 8 0 0 e. NN0
7 nnexpcl 
 |-  ( ( 2 e. NN /\ ; ; 8 0 0 e. NN0 ) -> ( 2 ^ ; ; 8 0 0 ) e. NN )
8 2 6 7 mp2an 
 |-  ( 2 ^ ; ; 8 0 0 ) e. NN
9 nnm1nn0 
 |-  ( ( 2 ^ ; ; 8 0 0 ) e. NN -> ( ( 2 ^ ; ; 8 0 0 ) - 1 ) e. NN0 )
10 8 9 ax-mp 
 |-  ( ( 2 ^ ; ; 8 0 0 ) - 1 ) e. NN0
11 2nn0 
 |-  2 e. NN0
12 3nn0 
 |-  3 e. NN0
13 11 12 deccl 
 |-  ; 2 3 e. NN0
14 1nn0 
 |-  1 e. NN0
15 13 14 deccl 
 |-  ; ; 2 3 1 e. NN0
16 15 4 deccl 
 |-  ; ; ; 2 3 1 0 e. NN0
17 4nn0 
 |-  4 e. NN0
18 17 4 deccl 
 |-  ; 4 0 e. NN0
19 18 4 deccl 
 |-  ; ; 4 0 0 e. NN0
20 1nn 
 |-  1 e. NN
21 19 20 decnncl 
 |-  ; ; ; 4 0 0 1 e. NN
22 1 21 eqeltri 
 |-  N e. NN
23 1 4001lem2 
 |-  ( ( 2 ^ ; ; 8 0 0 ) mod N ) = ( ; ; ; 2 3 1 1 mod N )
24 0p1e1 
 |-  ( 0 + 1 ) = 1
25 eqid 
 |-  ; ; ; 2 3 1 0 = ; ; ; 2 3 1 0
26 15 4 24 25 decsuc 
 |-  ( ; ; ; 2 3 1 0 + 1 ) = ; ; ; 2 3 1 1
27 22 8 14 16 23 26 modsubi 
 |-  ( ( ( 2 ^ ; ; 8 0 0 ) - 1 ) mod N ) = ( ; ; ; 2 3 1 0 mod N )
28 6nn0 
 |-  6 e. NN0
29 14 28 deccl 
 |-  ; 1 6 e. NN0
30 9nn0 
 |-  9 e. NN0
31 29 30 deccl 
 |-  ; ; 1 6 9 e. NN0
32 31 14 deccl 
 |-  ; ; ; 1 6 9 1 e. NN0
33 28 14 deccl 
 |-  ; 6 1 e. NN0
34 33 30 deccl 
 |-  ; ; 6 1 9 e. NN0
35 5nn0 
 |-  5 e. NN0
36 17 35 deccl 
 |-  ; 4 5 e. NN0
37 36 12 deccl 
 |-  ; ; 4 5 3 e. NN0
38 29 28 deccl 
 |-  ; ; 1 6 6 e. NN0
39 14 11 deccl 
 |-  ; 1 2 e. NN0
40 39 14 deccl 
 |-  ; ; 1 2 1 e. NN0
41 12 14 deccl 
 |-  ; 3 1 e. NN0
42 14 17 deccl 
 |-  ; 1 4 e. NN0
43 42 nn0zi 
 |-  ; 1 4 e. ZZ
44 12 nn0zi 
 |-  3 e. ZZ
45 gcdcom 
 |-  ( ( ; 1 4 e. ZZ /\ 3 e. ZZ ) -> ( ; 1 4 gcd 3 ) = ( 3 gcd ; 1 4 ) )
46 43 44 45 mp2an 
 |-  ( ; 1 4 gcd 3 ) = ( 3 gcd ; 1 4 )
47 3nn 
 |-  3 e. NN
48 4cn 
 |-  4 e. CC
49 3cn 
 |-  3 e. CC
50 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
51 48 49 50 mulcomli 
 |-  ( 3 x. 4 ) = ; 1 2
52 2p2e4 
 |-  ( 2 + 2 ) = 4
53 14 11 11 51 52 decaddi 
 |-  ( ( 3 x. 4 ) + 2 ) = ; 1 4
54 2lt3 
 |-  2 < 3
55 47 17 2 53 54 ndvdsi 
 |-  -. 3 || ; 1 4
56 3prm 
 |-  3 e. Prime
57 coprm 
 |-  ( ( 3 e. Prime /\ ; 1 4 e. ZZ ) -> ( -. 3 || ; 1 4 <-> ( 3 gcd ; 1 4 ) = 1 ) )
58 56 43 57 mp2an 
 |-  ( -. 3 || ; 1 4 <-> ( 3 gcd ; 1 4 ) = 1 )
59 55 58 mpbi 
 |-  ( 3 gcd ; 1 4 ) = 1
60 46 59 eqtri 
 |-  ( ; 1 4 gcd 3 ) = 1
61 eqid 
 |-  ; 1 4 = ; 1 4
62 12 dec0h 
 |-  3 = ; 0 3
63 2t1e2 
 |-  ( 2 x. 1 ) = 2
64 63 24 oveq12i 
 |-  ( ( 2 x. 1 ) + ( 0 + 1 ) ) = ( 2 + 1 )
65 2p1e3 
 |-  ( 2 + 1 ) = 3
66 64 65 eqtri 
 |-  ( ( 2 x. 1 ) + ( 0 + 1 ) ) = 3
67 2cn 
 |-  2 e. CC
68 4t2e8 
 |-  ( 4 x. 2 ) = 8
69 48 67 68 mulcomli 
 |-  ( 2 x. 4 ) = 8
70 69 oveq1i 
 |-  ( ( 2 x. 4 ) + 3 ) = ( 8 + 3 )
71 8p3e11 
 |-  ( 8 + 3 ) = ; 1 1
72 70 71 eqtri 
 |-  ( ( 2 x. 4 ) + 3 ) = ; 1 1
73 14 17 4 12 61 62 11 14 14 66 72 decma2c 
 |-  ( ( 2 x. ; 1 4 ) + 3 ) = ; 3 1
74 11 12 42 60 73 gcdi 
 |-  ( ; 3 1 gcd ; 1 4 ) = 1
75 eqid 
 |-  ; 3 1 = ; 3 1
76 49 mulid2i 
 |-  ( 1 x. 3 ) = 3
77 ax-1cn 
 |-  1 e. CC
78 77 addid1i 
 |-  ( 1 + 0 ) = 1
79 76 78 oveq12i 
 |-  ( ( 1 x. 3 ) + ( 1 + 0 ) ) = ( 3 + 1 )
80 3p1e4 
 |-  ( 3 + 1 ) = 4
81 79 80 eqtri 
 |-  ( ( 1 x. 3 ) + ( 1 + 0 ) ) = 4
82 1t1e1 
 |-  ( 1 x. 1 ) = 1
83 82 oveq1i 
 |-  ( ( 1 x. 1 ) + 4 ) = ( 1 + 4 )
84 4p1e5 
 |-  ( 4 + 1 ) = 5
85 48 77 84 addcomli 
 |-  ( 1 + 4 ) = 5
86 35 dec0h 
 |-  5 = ; 0 5
87 83 85 86 3eqtri 
 |-  ( ( 1 x. 1 ) + 4 ) = ; 0 5
88 12 14 14 17 75 61 14 35 4 81 87 decma2c 
 |-  ( ( 1 x. ; 3 1 ) + ; 1 4 ) = ; 4 5
89 14 42 41 74 88 gcdi 
 |-  ( ; 4 5 gcd ; 3 1 ) = 1
90 eqid 
 |-  ; 4 5 = ; 4 5
91 69 80 oveq12i 
 |-  ( ( 2 x. 4 ) + ( 3 + 1 ) ) = ( 8 + 4 )
92 8p4e12 
 |-  ( 8 + 4 ) = ; 1 2
93 91 92 eqtri 
 |-  ( ( 2 x. 4 ) + ( 3 + 1 ) ) = ; 1 2
94 5cn 
 |-  5 e. CC
95 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
96 94 67 95 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
97 14 4 24 96 decsuc 
 |-  ( ( 2 x. 5 ) + 1 ) = ; 1 1
98 17 35 12 14 90 75 11 14 14 93 97 decma2c 
 |-  ( ( 2 x. ; 4 5 ) + ; 3 1 ) = ; ; 1 2 1
99 11 41 36 89 98 gcdi 
 |-  ( ; ; 1 2 1 gcd ; 4 5 ) = 1
100 eqid 
 |-  ; ; 1 2 1 = ; ; 1 2 1
101 eqid 
 |-  ; 1 2 = ; 1 2
102 48 addid1i 
 |-  ( 4 + 0 ) = 4
103 17 dec0h 
 |-  4 = ; 0 4
104 102 103 eqtri 
 |-  ( 4 + 0 ) = ; 0 4
105 00id 
 |-  ( 0 + 0 ) = 0
106 82 105 oveq12i 
 |-  ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
107 106 78 eqtri 
 |-  ( ( 1 x. 1 ) + ( 0 + 0 ) ) = 1
108 67 mulid2i 
 |-  ( 1 x. 2 ) = 2
109 108 oveq1i 
 |-  ( ( 1 x. 2 ) + 4 ) = ( 2 + 4 )
110 4p2e6 
 |-  ( 4 + 2 ) = 6
111 48 67 110 addcomli 
 |-  ( 2 + 4 ) = 6
112 28 dec0h 
 |-  6 = ; 0 6
113 109 111 112 3eqtri 
 |-  ( ( 1 x. 2 ) + 4 ) = ; 0 6
114 14 11 4 17 101 104 14 28 4 107 113 decma2c 
 |-  ( ( 1 x. ; 1 2 ) + ( 4 + 0 ) ) = ; 1 6
115 82 oveq1i 
 |-  ( ( 1 x. 1 ) + 5 ) = ( 1 + 5 )
116 5p1e6 
 |-  ( 5 + 1 ) = 6
117 94 77 116 addcomli 
 |-  ( 1 + 5 ) = 6
118 115 117 112 3eqtri 
 |-  ( ( 1 x. 1 ) + 5 ) = ; 0 6
119 39 14 17 35 100 90 14 28 4 114 118 decma2c 
 |-  ( ( 1 x. ; ; 1 2 1 ) + ; 4 5 ) = ; ; 1 6 6
120 14 36 40 99 119 gcdi 
 |-  ( ; ; 1 6 6 gcd ; ; 1 2 1 ) = 1
121 eqid 
 |-  ; ; 1 6 6 = ; ; 1 6 6
122 eqid 
 |-  ; 1 6 = ; 1 6
123 14 11 65 101 decsuc 
 |-  ( ; 1 2 + 1 ) = ; 1 3
124 1p1e2 
 |-  ( 1 + 1 ) = 2
125 63 124 oveq12i 
 |-  ( ( 2 x. 1 ) + ( 1 + 1 ) ) = ( 2 + 2 )
126 125 52 eqtri 
 |-  ( ( 2 x. 1 ) + ( 1 + 1 ) ) = 4
127 6cn 
 |-  6 e. CC
128 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
129 127 67 128 mulcomli 
 |-  ( 2 x. 6 ) = ; 1 2
130 3p2e5 
 |-  ( 3 + 2 ) = 5
131 49 67 130 addcomli 
 |-  ( 2 + 3 ) = 5
132 14 11 12 129 131 decaddi 
 |-  ( ( 2 x. 6 ) + 3 ) = ; 1 5
133 14 28 14 12 122 123 11 35 14 126 132 decma2c 
 |-  ( ( 2 x. ; 1 6 ) + ( ; 1 2 + 1 ) ) = ; 4 5
134 14 11 65 129 decsuc 
 |-  ( ( 2 x. 6 ) + 1 ) = ; 1 3
135 29 28 39 14 121 100 11 12 14 133 134 decma2c 
 |-  ( ( 2 x. ; ; 1 6 6 ) + ; ; 1 2 1 ) = ; ; 4 5 3
136 11 40 38 120 135 gcdi 
 |-  ( ; ; 4 5 3 gcd ; ; 1 6 6 ) = 1
137 eqid 
 |-  ; ; 4 5 3 = ; ; 4 5 3
138 29 nn0cni 
 |-  ; 1 6 e. CC
139 138 addid1i 
 |-  ( ; 1 6 + 0 ) = ; 1 6
140 48 mulid2i 
 |-  ( 1 x. 4 ) = 4
141 140 124 oveq12i 
 |-  ( ( 1 x. 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
142 141 110 eqtri 
 |-  ( ( 1 x. 4 ) + ( 1 + 1 ) ) = 6
143 94 mulid2i 
 |-  ( 1 x. 5 ) = 5
144 143 oveq1i 
 |-  ( ( 1 x. 5 ) + 6 ) = ( 5 + 6 )
145 6p5e11 
 |-  ( 6 + 5 ) = ; 1 1
146 127 94 145 addcomli 
 |-  ( 5 + 6 ) = ; 1 1
147 144 146 eqtri 
 |-  ( ( 1 x. 5 ) + 6 ) = ; 1 1
148 17 35 14 28 90 139 14 14 14 142 147 decma2c 
 |-  ( ( 1 x. ; 4 5 ) + ( ; 1 6 + 0 ) ) = ; 6 1
149 76 oveq1i 
 |-  ( ( 1 x. 3 ) + 6 ) = ( 3 + 6 )
150 6p3e9 
 |-  ( 6 + 3 ) = 9
151 127 49 150 addcomli 
 |-  ( 3 + 6 ) = 9
152 30 dec0h 
 |-  9 = ; 0 9
153 149 151 152 3eqtri 
 |-  ( ( 1 x. 3 ) + 6 ) = ; 0 9
154 36 12 29 28 137 121 14 30 4 148 153 decma2c 
 |-  ( ( 1 x. ; ; 4 5 3 ) + ; ; 1 6 6 ) = ; ; 6 1 9
155 14 38 37 136 154 gcdi 
 |-  ( ; ; 6 1 9 gcd ; ; 4 5 3 ) = 1
156 eqid 
 |-  ; ; 6 1 9 = ; ; 6 1 9
157 7nn0 
 |-  7 e. NN0
158 eqid 
 |-  ; 6 1 = ; 6 1
159 5p2e7 
 |-  ( 5 + 2 ) = 7
160 17 35 11 90 159 decaddi 
 |-  ( ; 4 5 + 2 ) = ; 4 7
161 102 oveq2i 
 |-  ( ( 2 x. 6 ) + ( 4 + 0 ) ) = ( ( 2 x. 6 ) + 4 )
162 14 11 17 129 111 decaddi 
 |-  ( ( 2 x. 6 ) + 4 ) = ; 1 6
163 161 162 eqtri 
 |-  ( ( 2 x. 6 ) + ( 4 + 0 ) ) = ; 1 6
164 63 oveq1i 
 |-  ( ( 2 x. 1 ) + 7 ) = ( 2 + 7 )
165 7cn 
 |-  7 e. CC
166 7p2e9 
 |-  ( 7 + 2 ) = 9
167 165 67 166 addcomli 
 |-  ( 2 + 7 ) = 9
168 164 167 152 3eqtri 
 |-  ( ( 2 x. 1 ) + 7 ) = ; 0 9
169 28 14 17 157 158 160 11 30 4 163 168 decma2c 
 |-  ( ( 2 x. ; 6 1 ) + ( ; 4 5 + 2 ) ) = ; ; 1 6 9
170 9cn 
 |-  9 e. CC
171 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
172 170 67 171 mulcomli 
 |-  ( 2 x. 9 ) = ; 1 8
173 14 3 12 172 124 14 71 decaddci 
 |-  ( ( 2 x. 9 ) + 3 ) = ; 2 1
174 33 30 36 12 156 137 11 14 11 169 173 decma2c 
 |-  ( ( 2 x. ; ; 6 1 9 ) + ; ; 4 5 3 ) = ; ; ; 1 6 9 1
175 11 37 34 155 174 gcdi 
 |-  ( ; ; ; 1 6 9 1 gcd ; ; 6 1 9 ) = 1
176 eqid 
 |-  ; ; ; 1 6 9 1 = ; ; ; 1 6 9 1
177 eqid 
 |-  ; ; 1 6 9 = ; ; 1 6 9
178 28 14 124 158 decsuc 
 |-  ( ; 6 1 + 1 ) = ; 6 2
179 6p1e7 
 |-  ( 6 + 1 ) = 7
180 157 dec0h 
 |-  7 = ; 0 7
181 179 180 eqtri 
 |-  ( 6 + 1 ) = ; 0 7
182 82 24 oveq12i 
 |-  ( ( 1 x. 1 ) + ( 0 + 1 ) ) = ( 1 + 1 )
183 182 124 eqtri 
 |-  ( ( 1 x. 1 ) + ( 0 + 1 ) ) = 2
184 127 mulid2i 
 |-  ( 1 x. 6 ) = 6
185 184 oveq1i 
 |-  ( ( 1 x. 6 ) + 7 ) = ( 6 + 7 )
186 7p6e13 
 |-  ( 7 + 6 ) = ; 1 3
187 165 127 186 addcomli 
 |-  ( 6 + 7 ) = ; 1 3
188 185 187 eqtri 
 |-  ( ( 1 x. 6 ) + 7 ) = ; 1 3
189 14 28 4 157 122 181 14 12 14 183 188 decma2c 
 |-  ( ( 1 x. ; 1 6 ) + ( 6 + 1 ) ) = ; 2 3
190 170 mulid2i 
 |-  ( 1 x. 9 ) = 9
191 190 oveq1i 
 |-  ( ( 1 x. 9 ) + 2 ) = ( 9 + 2 )
192 9p2e11 
 |-  ( 9 + 2 ) = ; 1 1
193 191 192 eqtri 
 |-  ( ( 1 x. 9 ) + 2 ) = ; 1 1
194 29 30 28 11 177 178 14 14 14 189 193 decma2c 
 |-  ( ( 1 x. ; ; 1 6 9 ) + ( ; 6 1 + 1 ) ) = ; ; 2 3 1
195 82 oveq1i 
 |-  ( ( 1 x. 1 ) + 9 ) = ( 1 + 9 )
196 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
197 170 77 196 addcomli 
 |-  ( 1 + 9 ) = ; 1 0
198 195 197 eqtri 
 |-  ( ( 1 x. 1 ) + 9 ) = ; 1 0
199 31 14 33 30 176 156 14 4 14 194 198 decma2c 
 |-  ( ( 1 x. ; ; ; 1 6 9 1 ) + ; ; 6 1 9 ) = ; ; ; 2 3 1 0
200 14 34 32 175 199 gcdi 
 |-  ( ; ; ; 2 3 1 0 gcd ; ; ; 1 6 9 1 ) = 1
201 eqid 
 |-  ; ; 2 3 1 = ; ; 2 3 1
202 31 nn0cni 
 |-  ; ; 1 6 9 e. CC
203 202 addid1i 
 |-  ( ; ; 1 6 9 + 0 ) = ; ; 1 6 9
204 eqid 
 |-  ; 2 3 = ; 2 3
205 14 28 179 122 decsuc 
 |-  ( ; 1 6 + 1 ) = ; 1 7
206 108 124 oveq12i 
 |-  ( ( 1 x. 2 ) + ( 1 + 1 ) ) = ( 2 + 2 )
207 206 52 eqtri 
 |-  ( ( 1 x. 2 ) + ( 1 + 1 ) ) = 4
208 76 oveq1i 
 |-  ( ( 1 x. 3 ) + 7 ) = ( 3 + 7 )
209 7p3e10 
 |-  ( 7 + 3 ) = ; 1 0
210 165 49 209 addcomli 
 |-  ( 3 + 7 ) = ; 1 0
211 208 210 eqtri 
 |-  ( ( 1 x. 3 ) + 7 ) = ; 1 0
212 11 12 14 157 204 205 14 4 14 207 211 decma2c 
 |-  ( ( 1 x. ; 2 3 ) + ( ; 1 6 + 1 ) ) = ; 4 0
213 13 14 29 30 201 203 14 4 14 212 198 decma2c 
 |-  ( ( 1 x. ; ; 2 3 1 ) + ( ; ; 1 6 9 + 0 ) ) = ; ; 4 0 0
214 77 mul01i 
 |-  ( 1 x. 0 ) = 0
215 214 oveq1i 
 |-  ( ( 1 x. 0 ) + 1 ) = ( 0 + 1 )
216 14 dec0h 
 |-  1 = ; 0 1
217 215 24 216 3eqtri 
 |-  ( ( 1 x. 0 ) + 1 ) = ; 0 1
218 15 4 31 14 25 176 14 14 4 213 217 decma2c 
 |-  ( ( 1 x. ; ; ; 2 3 1 0 ) + ; ; ; 1 6 9 1 ) = ; ; ; 4 0 0 1
219 218 1 eqtr4i 
 |-  ( ( 1 x. ; ; ; 2 3 1 0 ) + ; ; ; 1 6 9 1 ) = N
220 14 32 16 200 219 gcdi 
 |-  ( N gcd ; ; ; 2 3 1 0 ) = 1
221 10 16 22 27 220 gcdmodi 
 |-  ( ( ( 2 ^ ; ; 8 0 0 ) - 1 ) gcd N ) = 1