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