# 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 $⊢ N = 2503$
Assertion 2503lem3 $⊢ 2 18 − 1 gcd N = 1$

### Proof

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