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