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 ⊢ 𝑁 = 4 0 0 1
Assertion 4001lem4 ( ( ( 2 ↑ 8 0 0 ) − 1 ) gcd 𝑁 ) = 1

Proof

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