Metamath Proof Explorer

Theorem 2503lem3

Description: Lemma for 2503prm . Calculate the GCD of 2 ^ 1 8 - 1 == 1 8 3 1 with N = 2 5 0 3 . (Contributed by Mario Carneiro, 3-Mar-2014) (Revised by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Hypothesis 2503prm.1 ⊢ 𝑁 = 2 5 0 3
Assertion 2503lem3 ( ( ( 2 ↑ 1 8 ) − 1 ) gcd 𝑁 ) = 1

Proof

Step Hyp Ref Expression
1 2503prm.1 ⊢ 𝑁 = 2 5 0 3
2 2nn ⊢ 2 ∈ ℕ
3 1nn0 ⊢ 1 ∈ ℕ0
4 8nn0 ⊢ 8 ∈ ℕ0
5 3 4 deccl ⊢ 1 8 ∈ ℕ0
6 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 1 8 ∈ ℕ0 ) → ( 2 ↑ 1 8 ) ∈ ℕ )
7 2 5 6 mp2an ⊢ ( 2 ↑ 1 8 ) ∈ ℕ
8 nnm1nn0 ⊢ ( ( 2 ↑ 1 8 ) ∈ ℕ → ( ( 2 ↑ 1 8 ) − 1 ) ∈ ℕ0 )
9 7 8 ax-mp ⊢ ( ( 2 ↑ 1 8 ) − 1 ) ∈ ℕ0
10 3nn0 ⊢ 3 ∈ ℕ0
11 5 10 deccl ⊢ 1 8 3 ∈ ℕ0
12 11 3 deccl ⊢ 1 8 3 1 ∈ ℕ0
13 2nn0 ⊢ 2 ∈ ℕ0
14 5nn0 ⊢ 5 ∈ ℕ0
15 13 14 deccl ⊢ 2 5 ∈ ℕ0
16 0nn0 ⊢ 0 ∈ ℕ0
17 15 16 deccl ⊢ 2 5 0 ∈ ℕ0
18 3nn ⊢ 3 ∈ ℕ
19 17 18 decnncl ⊢ 2 5 0 3 ∈ ℕ
20 1 19 eqeltri ⊢ 𝑁 ∈ ℕ
21 1 2503lem1 ⊢ ( ( 2 ↑ 1 8 ) mod 𝑁 ) = ( 1 8 3 2 mod 𝑁 )
22 1p1e2 ⊢ ( 1 + 1 ) = 2
23 eqid ⊢ 1 8 3 1 = 1 8 3 1
24 11 3 22 23 decsuc ⊢ ( 1 8 3 1 + 1 ) = 1 8 3 2
25 20 7 3 12 21 24 modsubi ⊢ ( ( ( 2 ↑ 1 8 ) − 1 ) mod 𝑁 ) = ( 1 8 3 1 mod 𝑁 )
26 6nn0 ⊢ 6 ∈ ℕ0
27 7nn0 ⊢ 7 ∈ ℕ0
28 26 27 deccl ⊢ 6 7 ∈ ℕ0
29 28 13 deccl ⊢ 6 7 2 ∈ ℕ0
30 4nn0 ⊢ 4 ∈ ℕ0
31 30 4 deccl ⊢ 4 8 ∈ ℕ0
32 31 27 deccl ⊢ 4 8 7 ∈ ℕ0
33 5 14 deccl ⊢ 1 8 5 ∈ ℕ0
34 3 3 deccl ⊢ 1 1 ∈ ℕ0
35 34 27 deccl ⊢ 1 1 7 ∈ ℕ0
36 26 4 deccl ⊢ 6 8 ∈ ℕ0
37 9nn0 ⊢ 9 ∈ ℕ0
38 30 37 deccl ⊢ 4 9 ∈ ℕ0
39 3 37 deccl ⊢ 1 9 ∈ ℕ0
40 38 nn0zi ⊢ 4 9 ∈ ℤ
41 39 nn0zi ⊢ 1 9 ∈ ℤ
42 gcdcom ⊢ ( ( 4 9 ∈ ℤ ∧ 1 9 ∈ ℤ ) → ( 4 9 gcd 1 9 ) = ( 1 9 gcd 4 9 ) )
43 40 41 42 mp2an ⊢ ( 4 9 gcd 1 9 ) = ( 1 9 gcd 4 9 )
44 9nn ⊢ 9 ∈ ℕ
45 3 44 decnncl ⊢ 1 9 ∈ ℕ
46 1nn ⊢ 1 ∈ ℕ
47 3 46 decnncl ⊢ 1 1 ∈ ℕ
48 eqid ⊢ 1 9 = 1 9
49 eqid ⊢ 1 1 = 1 1
50 2cn ⊢ 2 ∈ ℂ
51 50 mullidi ⊢ ( 1 · 2 ) = 2
52 51 22 oveq12i ⊢ ( ( 1 · 2 ) + ( 1 + 1 ) ) = ( 2 + 2 )
53 2p2e4 ⊢ ( 2 + 2 ) = 4
54 52 53 eqtri ⊢ ( ( 1 · 2 ) + ( 1 + 1 ) ) = 4
55 8p1e9 ⊢ ( 8 + 1 ) = 9
56 9t2e18 ⊢ ( 9 · 2 ) = 1 8
57 3 4 55 56 decsuc ⊢ ( ( 9 · 2 ) + 1 ) = 1 9
58 3 37 3 3 48 49 13 37 3 54 57 decmac ⊢ ( ( 1 9 · 2 ) + 1 1 ) = 4 9
59 1lt9 ⊢ 1 < 9
60 3 3 44 59 declt ⊢ 1 1 < 1 9
61 45 13 47 58 60 ndvdsi ⊢ ¬ 1 9 ∥ 4 9
62 19prm ⊢ 1 9 ∈ ℙ
63 coprm ⊢ ( ( 1 9 ∈ ℙ ∧ 4 9 ∈ ℤ ) → ( ¬ 1 9 ∥ 4 9 ↔ ( 1 9 gcd 4 9 ) = 1 ) )
64 62 40 63 mp2an ⊢ ( ¬ 1 9 ∥ 4 9 ↔ ( 1 9 gcd 4 9 ) = 1 )
65 61 64 mpbi ⊢ ( 1 9 gcd 4 9 ) = 1
66 43 65 eqtri ⊢ ( 4 9 gcd 1 9 ) = 1
67 eqid ⊢ 4 9 = 4 9
68 4cn ⊢ 4 ∈ ℂ
69 68 mullidi ⊢ ( 1 · 4 ) = 4
70 69 22 oveq12i ⊢ ( ( 1 · 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
71 4p2e6 ⊢ ( 4 + 2 ) = 6
72 70 71 eqtri ⊢ ( ( 1 · 4 ) + ( 1 + 1 ) ) = 6
73 9cn ⊢ 9 ∈ ℂ
74 73 mullidi ⊢ ( 1 · 9 ) = 9
75 74 oveq1i ⊢ ( ( 1 · 9 ) + 9 ) = ( 9 + 9 )
76 9p9e18 ⊢ ( 9 + 9 ) = 1 8
77 75 76 eqtri ⊢ ( ( 1 · 9 ) + 9 ) = 1 8
78 30 37 3 37 67 48 3 4 3 72 77 decma2c ⊢ ( ( 1 · 4 9 ) + 1 9 ) = 6 8
79 3 39 38 66 78 gcdi ⊢ ( 6 8 gcd 4 9 ) = 1
80 eqid ⊢ 6 8 = 6 8
81 6cn ⊢ 6 ∈ ℂ
82 81 mullidi ⊢ ( 1 · 6 ) = 6
83 4p1e5 ⊢ ( 4 + 1 ) = 5
84 82 83 oveq12i ⊢ ( ( 1 · 6 ) + ( 4 + 1 ) ) = ( 6 + 5 )
85 6p5e11 ⊢ ( 6 + 5 ) = 1 1
86 84 85 eqtri ⊢ ( ( 1 · 6 ) + ( 4 + 1 ) ) = 1 1
87 8cn ⊢ 8 ∈ ℂ
88 87 mullidi ⊢ ( 1 · 8 ) = 8
89 88 oveq1i ⊢ ( ( 1 · 8 ) + 9 ) = ( 8 + 9 )
90 9p8e17 ⊢ ( 9 + 8 ) = 1 7
91 73 87 90 addcomli ⊢ ( 8 + 9 ) = 1 7
92 89 91 eqtri ⊢ ( ( 1 · 8 ) + 9 ) = 1 7
93 26 4 30 37 80 67 3 27 3 86 92 decma2c ⊢ ( ( 1 · 6 8 ) + 4 9 ) = 1 1 7
94 3 38 36 79 93 gcdi ⊢ ( 1 1 7 gcd 6 8 ) = 1
95 eqid ⊢ 1 1 7 = 1 1 7
96 6p1e7 ⊢ ( 6 + 1 ) = 7
97 27 dec0h ⊢ 7 = 0 7
98 96 97 eqtri ⊢ ( 6 + 1 ) = 0 7
99 1t1e1 ⊢ ( 1 · 1 ) = 1
100 00id ⊢ ( 0 + 0 ) = 0
101 99 100 oveq12i ⊢ ( ( 1 · 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
102 ax-1cn ⊢ 1 ∈ ℂ
103 102 addridi ⊢ ( 1 + 0 ) = 1
104 101 103 eqtri ⊢ ( ( 1 · 1 ) + ( 0 + 0 ) ) = 1
105 99 oveq1i ⊢ ( ( 1 · 1 ) + 7 ) = ( 1 + 7 )
106 7cn ⊢ 7 ∈ ℂ
107 7p1e8 ⊢ ( 7 + 1 ) = 8
108 106 102 107 addcomli ⊢ ( 1 + 7 ) = 8
109 4 dec0h ⊢ 8 = 0 8
110 105 108 109 3eqtri ⊢ ( ( 1 · 1 ) + 7 ) = 0 8
111 3 3 16 27 49 98 3 4 16 104 110 decma2c ⊢ ( ( 1 · 1 1 ) + ( 6 + 1 ) ) = 1 8
112 106 mullidi ⊢ ( 1 · 7 ) = 7
113 112 oveq1i ⊢ ( ( 1 · 7 ) + 8 ) = ( 7 + 8 )
114 8p7e15 ⊢ ( 8 + 7 ) = 1 5
115 87 106 114 addcomli ⊢ ( 7 + 8 ) = 1 5
116 113 115 eqtri ⊢ ( ( 1 · 7 ) + 8 ) = 1 5
117 34 27 26 4 95 80 3 14 3 111 116 decma2c ⊢ ( ( 1 · 1 1 7 ) + 6 8 ) = 1 8 5
118 3 36 35 94 117 gcdi ⊢ ( 1 8 5 gcd 1 1 7 ) = 1
119 eqid ⊢ 1 8 5 = 1 8 5
120 eqid ⊢ 1 8 = 1 8
121 3 3 22 49 decsuc ⊢ ( 1 1 + 1 ) = 1 2
122 2t1e2 ⊢ ( 2 · 1 ) = 2
123 122 22 oveq12i ⊢ ( ( 2 · 1 ) + ( 1 + 1 ) ) = ( 2 + 2 )
124 123 53 eqtri ⊢ ( ( 2 · 1 ) + ( 1 + 1 ) ) = 4
125 8t2e16 ⊢ ( 8 · 2 ) = 1 6
126 87 50 125 mulcomli ⊢ ( 2 · 8 ) = 1 6
127 6p2e8 ⊢ ( 6 + 2 ) = 8
128 3 26 13 126 127 decaddi ⊢ ( ( 2 · 8 ) + 2 ) = 1 8
129 3 4 3 13 120 121 13 4 3 124 128 decma2c ⊢ ( ( 2 · 1 8 ) + ( 1 1 + 1 ) ) = 4 8
130 5cn ⊢ 5 ∈ ℂ
131 5t2e10 ⊢ ( 5 · 2 ) = 1 0
132 130 50 131 mulcomli ⊢ ( 2 · 5 ) = 1 0
133 106 addlidi ⊢ ( 0 + 7 ) = 7
134 3 16 27 132 133 decaddi ⊢ ( ( 2 · 5 ) + 7 ) = 1 7
135 5 14 34 27 119 95 13 27 3 129 134 decma2c ⊢ ( ( 2 · 1 8 5 ) + 1 1 7 ) = 4 8 7
136 13 35 33 118 135 gcdi ⊢ ( 4 8 7 gcd 1 8 5 ) = 1
137 eqid ⊢ 4 8 7 = 4 8 7
138 eqid ⊢ 4 8 = 4 8
139 3 4 55 120 decsuc ⊢ ( 1 8 + 1 ) = 1 9
140 30 4 3 37 138 139 3 27 3 72 92 decma2c ⊢ ( ( 1 · 4 8 ) + ( 1 8 + 1 ) ) = 6 7
141 112 oveq1i ⊢ ( ( 1 · 7 ) + 5 ) = ( 7 + 5 )
142 7p5e12 ⊢ ( 7 + 5 ) = 1 2
143 141 142 eqtri ⊢ ( ( 1 · 7 ) + 5 ) = 1 2
144 31 27 5 14 137 119 3 13 3 140 143 decma2c ⊢ ( ( 1 · 4 8 7 ) + 1 8 5 ) = 6 7 2
145 3 33 32 136 144 gcdi ⊢ ( 6 7 2 gcd 4 8 7 ) = 1
146 eqid ⊢ 6 7 2 = 6 7 2
147 eqid ⊢ 6 7 = 6 7
148 30 4 55 138 decsuc ⊢ ( 4 8 + 1 ) = 4 9
149 71 oveq2i ⊢ ( ( 2 · 6 ) + ( 4 + 2 ) ) = ( ( 2 · 6 ) + 6 )
150 6t2e12 ⊢ ( 6 · 2 ) = 1 2
151 81 50 150 mulcomli ⊢ ( 2 · 6 ) = 1 2
152 81 50 127 addcomli ⊢ ( 2 + 6 ) = 8
153 3 13 26 151 152 decaddi ⊢ ( ( 2 · 6 ) + 6 ) = 1 8
154 149 153 eqtri ⊢ ( ( 2 · 6 ) + ( 4 + 2 ) ) = 1 8
155 7t2e14 ⊢ ( 7 · 2 ) = 1 4
156 106 50 155 mulcomli ⊢ ( 2 · 7 ) = 1 4
157 9p4e13 ⊢ ( 9 + 4 ) = 1 3
158 73 68 157 addcomli ⊢ ( 4 + 9 ) = 1 3
159 3 30 37 156 22 10 158 decaddci ⊢ ( ( 2 · 7 ) + 9 ) = 2 3
160 26 27 30 37 147 148 13 10 13 154 159 decma2c ⊢ ( ( 2 · 6 7 ) + ( 4 8 + 1 ) ) = 1 8 3
161 2t2e4 ⊢ ( 2 · 2 ) = 4
162 161 oveq1i ⊢ ( ( 2 · 2 ) + 7 ) = ( 4 + 7 )
163 7p4e11 ⊢ ( 7 + 4 ) = 1 1
164 106 68 163 addcomli ⊢ ( 4 + 7 ) = 1 1
165 162 164 eqtri ⊢ ( ( 2 · 2 ) + 7 ) = 1 1
166 28 13 31 27 146 137 13 3 3 160 165 decma2c ⊢ ( ( 2 · 6 7 2 ) + 4 8 7 ) = 1 8 3 1
167 13 32 29 145 166 gcdi ⊢ ( 1 8 3 1 gcd 6 7 2 ) = 1
168 eqid ⊢ 1 8 3 = 1 8 3
169 28 nn0cni ⊢ 6 7 ∈ ℂ
170 169 addridi ⊢ ( 6 7 + 0 ) = 6 7
171 102 addlidi ⊢ ( 0 + 1 ) = 1
172 99 171 oveq12i ⊢ ( ( 1 · 1 ) + ( 0 + 1 ) ) = ( 1 + 1 )
173 172 22 eqtri ⊢ ( ( 1 · 1 ) + ( 0 + 1 ) ) = 2
174 88 oveq1i ⊢ ( ( 1 · 8 ) + 7 ) = ( 8 + 7 )
175 174 114 eqtri ⊢ ( ( 1 · 8 ) + 7 ) = 1 5
176 3 4 16 27 120 98 3 14 3 173 175 decma2c ⊢ ( ( 1 · 1 8 ) + ( 6 + 1 ) ) = 2 5
177 3cn ⊢ 3 ∈ ℂ
178 177 mullidi ⊢ ( 1 · 3 ) = 3
179 178 oveq1i ⊢ ( ( 1 · 3 ) + 7 ) = ( 3 + 7 )
180 7p3e10 ⊢ ( 7 + 3 ) = 1 0
181 106 177 180 addcomli ⊢ ( 3 + 7 ) = 1 0
182 179 181 eqtri ⊢ ( ( 1 · 3 ) + 7 ) = 1 0
183 5 10 26 27 168 170 3 16 3 176 182 decma2c ⊢ ( ( 1 · 1 8 3 ) + ( 6 7 + 0 ) ) = 2 5 0
184 99 oveq1i ⊢ ( ( 1 · 1 ) + 2 ) = ( 1 + 2 )
185 1p2e3 ⊢ ( 1 + 2 ) = 3
186 10 dec0h ⊢ 3 = 0 3
187 184 185 186 3eqtri ⊢ ( ( 1 · 1 ) + 2 ) = 0 3
188 11 3 28 13 23 146 3 10 16 183 187 decma2c ⊢ ( ( 1 · 1 8 3 1 ) + 6 7 2 ) = 2 5 0 3
189 188 1 eqtr4i ⊢ ( ( 1 · 1 8 3 1 ) + 6 7 2 ) = 𝑁
190 3 29 12 167 189 gcdi ⊢ ( 𝑁 gcd 1 8 3 1 ) = 1
191 9 12 20 25 190 gcdmodi ⊢ ( ( ( 2 ↑ 1 8 ) − 1 ) gcd 𝑁 ) = 1