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	$$⊢\left(2^{18}-1\right)\gcd N=1$$

Proof

Step	Hyp	Ref	Expression
1		2503prm.1	$$⊢N=2503$$
2		2nn	$$⊢2\in \mathbb{N}$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		8nn0	$$⊢8\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢18\in {\mathbb{N}}_0$$
6		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge 18\in {\mathbb{N}}_0\right)\to 2^{18}\in \mathbb{N}$$
7	2 5 6	mp2an	$$⊢2^{18}\in \mathbb{N}$$
8		nnm1nn0	$$⊢2^{18}\in \mathbb{N}\to 2^{18}-1\in {\mathbb{N}}_0$$
9	7 8	ax-mp	$$⊢2^{18}-1\in {\mathbb{N}}_0$$
10		3nn0	$$⊢3\in {\mathbb{N}}_0$$
11	5 10	deccl	$$⊢183\in {\mathbb{N}}_0$$
12	11 3	deccl	$$⊢1831\in {\mathbb{N}}_0$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14		5nn0	$$⊢5\in {\mathbb{N}}_0$$
15	13 14	deccl	$$⊢25\in {\mathbb{N}}_0$$
16		0nn0	$$⊢0\in {\mathbb{N}}_0$$
17	15 16	deccl	$$⊢250\in {\mathbb{N}}_0$$
18		3nn	$$⊢3\in \mathbb{N}$$
19	17 18	decnncl	$$⊢2503\in \mathbb{N}$$
20	1 19	eqeltri	$$⊢N\in \mathbb{N}$$
21	1	2503lem1	$$⊢2^{18}\mathrm{mod}N=1832\mathrm{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	$$⊢\left(2^{18}-1\right)\mathrm{mod}N=1831\mathrm{mod}N$$
26		6nn0	$$⊢6\in {\mathbb{N}}_0$$
27		7nn0	$$⊢7\in {\mathbb{N}}_0$$
28	26 27	deccl	$$⊢67\in {\mathbb{N}}_0$$
29	28 13	deccl	$$⊢672\in {\mathbb{N}}_0$$
30		4nn0	$$⊢4\in {\mathbb{N}}_0$$
31	30 4	deccl	$$⊢48\in {\mathbb{N}}_0$$
32	31 27	deccl	$$⊢487\in {\mathbb{N}}_0$$
33	5 14	deccl	$$⊢185\in {\mathbb{N}}_0$$
34	3 3	deccl	$$⊢11\in {\mathbb{N}}_0$$
35	34 27	deccl	$$⊢117\in {\mathbb{N}}_0$$
36	26 4	deccl	$$⊢68\in {\mathbb{N}}_0$$
37		9nn0	$$⊢9\in {\mathbb{N}}_0$$
38	30 37	deccl	$$⊢49\in {\mathbb{N}}_0$$
39	3 37	deccl	$$⊢19\in {\mathbb{N}}_0$$
40	38	nn0zi	$$⊢49\in \mathbb{Z}$$
41	39	nn0zi	$$⊢19\in \mathbb{Z}$$
42		gcdcom	$$⊢\left(49\in \mathbb{Z}\wedge 19\in \mathbb{Z}\right)\to 49\gcd 19=19\gcd 49$$
43	40 41 42	mp2an	$$⊢49\gcd 19=19\gcd 49$$
44		9nn	$$⊢9\in \mathbb{N}$$
45	3 44	decnncl	$$⊢19\in \mathbb{N}$$
46		1nn	$$⊢1\in \mathbb{N}$$
47	3 46	decnncl	$$⊢11\in \mathbb{N}$$
48		eqid	$$⊢19=19$$
49		eqid	$$⊢11=11$$
50		2cn	$$⊢2\in ℂ$$
51	50	mullidi	$$⊢1\cdot 2=2$$
52	51 22	oveq12i	$$⊢1\cdot 2+1+1=2+2$$
53		2p2e4	$$⊢2+2=4$$
54	52 53	eqtri	$$⊢1\cdot 2+1+1=4$$
55		8p1e9	$$⊢8+1=9$$
56		9t2e18	$$⊢9\cdot 2=18$$
57	3 4 55 56	decsuc	$$⊢9\cdot 2+1=19$$
58	3 37 3 3 48 49 13 37 3 54 57	decmac	$$⊢19\cdot 2+11=49$$
59		1lt9	$$⊢1<9$$
60	3 3 44 59	declt	$$⊢11<19$$
61	45 13 47 58 60	ndvdsi	$$⊢\neg 19\parallel 49$$
62		19prm	$$⊢19\in \mathbb{P}$$
63		coprm	$$⊢\left(19\in \mathbb{P}\wedge 49\in \mathbb{Z}\right)\to \left(\neg 19\parallel 49\leftrightarrow 19\gcd 49=1\right)$$
64	62 40 63	mp2an	$$⊢\neg 19\parallel 49\leftrightarrow 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\in ℂ$$
69	68	mullidi	$$⊢1\cdot 4=4$$
70	69 22	oveq12i	$$⊢1\cdot 4+1+1=4+2$$
71		4p2e6	$$⊢4+2=6$$
72	70 71	eqtri	$$⊢1\cdot 4+1+1=6$$
73		9cn	$$⊢9\in ℂ$$
74	73	mullidi	$$⊢1\cdot 9=9$$
75	74	oveq1i	$$⊢1\cdot 9+9=9+9$$
76		9p9e18	$$⊢9+9=18$$
77	75 76	eqtri	$$⊢1\cdot 9+9=18$$
78	30 37 3 37 67 48 3 4 3 72 77	decma2c	$$⊢1\cdot 49+19=68$$
79	3 39 38 66 78	gcdi	$$⊢68\gcd 49=1$$
80		eqid	$$⊢68=68$$
81		6cn	$$⊢6\in ℂ$$
82	81	mullidi	$$⊢1\cdot 6=6$$
83		4p1e5	$$⊢4+1=5$$
84	82 83	oveq12i	$$⊢1\cdot 6+4+1=6+5$$
85		6p5e11	$$⊢6+5=11$$
86	84 85	eqtri	$$⊢1\cdot 6+4+1=11$$
87		8cn	$$⊢8\in ℂ$$
88	87	mullidi	$$⊢1\cdot 8=8$$
89	88	oveq1i	$$⊢1\cdot 8+9=8+9$$
90		9p8e17	$$⊢9+8=17$$
91	73 87 90	addcomli	$$⊢8+9=17$$
92	89 91	eqtri	$$⊢1\cdot 8+9=17$$
93	26 4 30 37 80 67 3 27 3 86 92	decma2c	$$⊢1\cdot 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\cdot 1=1$$
100		00id	$$⊢0+0=0$$
101	99 100	oveq12i	$$⊢1\cdot 1+0+0=1+0$$
102		ax-1cn	$$⊢1\in ℂ$$
103	102	addridi	$$⊢1+0=1$$
104	101 103	eqtri	$$⊢1\cdot 1+0+0=1$$
105	99	oveq1i	$$⊢1\cdot 1+7=1+7$$
106		7cn	$$⊢7\in ℂ$$
107		7p1e8	$$⊢7+1=8$$
108	106 102 107	addcomli	$$⊢1+7=8$$
109	4	dec0h	$$⊢8=08$$
110	105 108 109	3eqtri	$$⊢1\cdot 1+7=08$$
111	3 3 16 27 49 98 3 4 16 104 110	decma2c	$$⊢1\cdot 11+6+1=18$$
112	106	mullidi	$$⊢1\cdot 7=7$$
113	112	oveq1i	$$⊢1\cdot 7+8=7+8$$
114		8p7e15	$$⊢8+7=15$$
115	87 106 114	addcomli	$$⊢7+8=15$$
116	113 115	eqtri	$$⊢1\cdot 7+8=15$$
117	34 27 26 4 95 80 3 14 3 111 116	decma2c	$$⊢1\cdot 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\cdot 1=2$$
123	122 22	oveq12i	$$⊢2\cdot 1+1+1=2+2$$
124	123 53	eqtri	$$⊢2\cdot 1+1+1=4$$
125		8t2e16	$$⊢8\cdot 2=16$$
126	87 50 125	mulcomli	$$⊢2\cdot 8=16$$
127		6p2e8	$$⊢6+2=8$$
128	3 26 13 126 127	decaddi	$$⊢2\cdot 8+2=18$$
129	3 4 3 13 120 121 13 4 3 124 128	decma2c	$$⊢2\cdot 18+11+1=48$$
130		5cn	$$⊢5\in ℂ$$
131		5t2e10	$$⊢5\cdot 2=10$$
132	130 50 131	mulcomli	$$⊢2\cdot 5=10$$
133	106	addlidi	$$⊢0+7=7$$
134	3 16 27 132 133	decaddi	$$⊢2\cdot 5+7=17$$
135	5 14 34 27 119 95 13 27 3 129 134	decma2c	$$⊢2\cdot 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\cdot 48+18+1=67$$
141	112	oveq1i	$$⊢1\cdot 7+5=7+5$$
142		7p5e12	$$⊢7+5=12$$
143	141 142	eqtri	$$⊢1\cdot 7+5=12$$
144	31 27 5 14 137 119 3 13 3 140 143	decma2c	$$⊢1\cdot 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\cdot 6+4+2=2\cdot 6+6$$
150		6t2e12	$$⊢6\cdot 2=12$$
151	81 50 150	mulcomli	$$⊢2\cdot 6=12$$
152	81 50 127	addcomli	$$⊢2+6=8$$
153	3 13 26 151 152	decaddi	$$⊢2\cdot 6+6=18$$
154	149 153	eqtri	$$⊢2\cdot 6+4+2=18$$
155		7t2e14	$$⊢7\cdot 2=14$$
156	106 50 155	mulcomli	$$⊢2\cdot 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\cdot 7+9=23$$
160	26 27 30 37 147 148 13 10 13 154 159	decma2c	$$⊢2\cdot 67+48+1=183$$
161		2t2e4	$$⊢2\cdot 2=4$$
162	161	oveq1i	$$⊢2\cdot 2+7=4+7$$
163		7p4e11	$$⊢7+4=11$$
164	106 68 163	addcomli	$$⊢4+7=11$$
165	162 164	eqtri	$$⊢2\cdot 2+7=11$$
166	28 13 31 27 146 137 13 3 3 160 165	decma2c	$$⊢2\cdot 672+487=1831$$
167	13 32 29 145 166	gcdi	$$⊢1831\gcd 672=1$$
168		eqid	$$⊢183=183$$
169	28	nn0cni	$$⊢67\in ℂ$$
170	169	addridi	$$⊢67+0=67$$
171	102	addlidi	$$⊢0+1=1$$
172	99 171	oveq12i	$$⊢1\cdot 1+0+1=1+1$$
173	172 22	eqtri	$$⊢1\cdot 1+0+1=2$$
174	88	oveq1i	$$⊢1\cdot 8+7=8+7$$
175	174 114	eqtri	$$⊢1\cdot 8+7=15$$
176	3 4 16 27 120 98 3 14 3 173 175	decma2c	$$⊢1\cdot 18+6+1=25$$
177		3cn	$$⊢3\in ℂ$$
178	177	mullidi	$$⊢1\cdot 3=3$$
179	178	oveq1i	$$⊢1\cdot 3+7=3+7$$
180		7p3e10	$$⊢7+3=10$$
181	106 177 180	addcomli	$$⊢3+7=10$$
182	179 181	eqtri	$$⊢1\cdot 3+7=10$$
183	5 10 26 27 168 170 3 16 3 176 182	decma2c	$$⊢1\cdot 183+67+0=250$$
184	99	oveq1i	$$⊢1\cdot 1+2=1+2$$
185		1p2e3	$$⊢1+2=3$$
186	10	dec0h	$$⊢3=03$$
187	184 185 186	3eqtri	$$⊢1\cdot 1+2=03$$
188	11 3 28 13 23 146 3 10 16 183 187	decma2c	$$⊢1\cdot 1831+672=2503$$
189	188 1	eqtr4i	$$⊢1\cdot 1831+672=N$$
190	3 29 12 167 189	gcdi	$$⊢N\gcd 1831=1$$
191	9 12 20 25 190	gcdmodi	$$⊢\left(2^{18}-1\right)\gcd N=1$$