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

Proof

Step	Hyp	Ref	Expression
1		4001prm.1	$$⊢N=4001$$
2		2nn	$$⊢2\in \mathbb{N}$$
3		8nn0	$$⊢8\in {\mathbb{N}}_0$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢80\in {\mathbb{N}}_0$$
6	5 4	deccl	$$⊢800\in {\mathbb{N}}_0$$
7		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge 800\in {\mathbb{N}}_0\right)\to 2^{800}\in \mathbb{N}$$
8	2 6 7	mp2an	$$⊢2^{800}\in \mathbb{N}$$
9		nnm1nn0	$$⊢2^{800}\in \mathbb{N}\to 2^{800}-1\in {\mathbb{N}}_0$$
10	8 9	ax-mp	$$⊢2^{800}-1\in {\mathbb{N}}_0$$
11		2nn0	$$⊢2\in {\mathbb{N}}_0$$
12		3nn0	$$⊢3\in {\mathbb{N}}_0$$
13	11 12	deccl	$$⊢23\in {\mathbb{N}}_0$$
14		1nn0	$$⊢1\in {\mathbb{N}}_0$$
15	13 14	deccl	$$⊢231\in {\mathbb{N}}_0$$
16	15 4	deccl	$$⊢2310\in {\mathbb{N}}_0$$
17		4nn0	$$⊢4\in {\mathbb{N}}_0$$
18	17 4	deccl	$$⊢40\in {\mathbb{N}}_0$$
19	18 4	deccl	$$⊢400\in {\mathbb{N}}_0$$
20		1nn	$$⊢1\in \mathbb{N}$$
21	19 20	decnncl	$$⊢4001\in \mathbb{N}$$
22	1 21	eqeltri	$$⊢N\in \mathbb{N}$$
23	1	4001lem2	$$⊢2^{800}\mathrm{mod}N=2311\mathrm{mod}N$$
24		0p1e1	$$⊢0+1=1$$
25		eqid	$$⊢2310=2310$$
26	15 4 24 25	decsuc	$$⊢2310+1=2311$$
27	22 8 14 16 23 26	modsubi	$$⊢\left(2^{800}-1\right)\mathrm{mod}N=2310\mathrm{mod}N$$
28		6nn0	$$⊢6\in {\mathbb{N}}_0$$
29	14 28	deccl	$$⊢16\in {\mathbb{N}}_0$$
30		9nn0	$$⊢9\in {\mathbb{N}}_0$$
31	29 30	deccl	$$⊢169\in {\mathbb{N}}_0$$
32	31 14	deccl	$$⊢1691\in {\mathbb{N}}_0$$
33	28 14	deccl	$$⊢61\in {\mathbb{N}}_0$$
34	33 30	deccl	$$⊢619\in {\mathbb{N}}_0$$
35		5nn0	$$⊢5\in {\mathbb{N}}_0$$
36	17 35	deccl	$$⊢45\in {\mathbb{N}}_0$$
37	36 12	deccl	$$⊢453\in {\mathbb{N}}_0$$
38	29 28	deccl	$$⊢166\in {\mathbb{N}}_0$$
39	14 11	deccl	$$⊢12\in {\mathbb{N}}_0$$
40	39 14	deccl	$$⊢121\in {\mathbb{N}}_0$$
41	12 14	deccl	$$⊢31\in {\mathbb{N}}_0$$
42	14 17	deccl	$$⊢14\in {\mathbb{N}}_0$$
43	42	nn0zi	$$⊢14\in \mathbb{Z}$$
44	12	nn0zi	$$⊢3\in \mathbb{Z}$$
45		gcdcom	$$⊢\left(14\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to 14\gcd 3=3\gcd 14$$
46	43 44 45	mp2an	$$⊢14\gcd 3=3\gcd 14$$
47		3nn	$$⊢3\in \mathbb{N}$$
48		4cn	$$⊢4\in ℂ$$
49		3cn	$$⊢3\in ℂ$$
50		4t3e12	$$⊢4\cdot 3=12$$
51	48 49 50	mulcomli	$$⊢3\cdot 4=12$$
52		2p2e4	$$⊢2+2=4$$
53	14 11 11 51 52	decaddi	$$⊢3\cdot 4+2=14$$
54		2lt3	$$⊢2<3$$
55	47 17 2 53 54	ndvdsi	$$⊢\neg 3\parallel 14$$
56		3prm	$$⊢3\in \mathbb{P}$$
57		coprm	$$⊢\left(3\in \mathbb{P}\wedge 14\in \mathbb{Z}\right)\to \left(\neg 3\parallel 14\leftrightarrow 3\gcd 14=1\right)$$
58	56 43 57	mp2an	$$⊢\neg 3\parallel 14\leftrightarrow 3\gcd 14=1$$
59	55 58	mpbi	$$⊢3\gcd 14=1$$
60	46 59	eqtri	$$⊢14\gcd 3=1$$
61		eqid	$$⊢14=14$$
62	12	dec0h	$$⊢3=03$$
63		2t1e2	$$⊢2\cdot 1=2$$
64	63 24	oveq12i	$$⊢2\cdot 1+0+1=2+1$$
65		2p1e3	$$⊢2+1=3$$
66	64 65	eqtri	$$⊢2\cdot 1+0+1=3$$
67		2t4e8	$$⊢2\cdot 4=8$$
68	67	oveq1i	$$⊢2\cdot 4+3=8+3$$
69		8p3e11	$$⊢8+3=11$$
70	68 69	eqtri	$$⊢2\cdot 4+3=11$$
71	14 17 4 12 61 62 11 14 14 66 70	decma2c	$$⊢2\cdot 14+3=31$$
72	11 12 42 60 71	gcdi	$$⊢31\gcd 14=1$$
73		eqid	$$⊢31=31$$
74	49	mullidi	$$⊢1\cdot 3=3$$
75		ax-1cn	$$⊢1\in ℂ$$
76	75	addridi	$$⊢1+0=1$$
77	74 76	oveq12i	$$⊢1\cdot 3+1+0=3+1$$
78		3p1e4	$$⊢3+1=4$$
79	77 78	eqtri	$$⊢1\cdot 3+1+0=4$$
80		1t1e1	$$⊢1\cdot 1=1$$
81	80	oveq1i	$$⊢1\cdot 1+4=1+4$$
82		4p1e5	$$⊢4+1=5$$
83	48 75 82	addcomli	$$⊢1+4=5$$
84	35	dec0h	$$⊢5=05$$
85	81 83 84	3eqtri	$$⊢1\cdot 1+4=05$$
86	12 14 14 17 73 61 14 35 4 79 85	decma2c	$$⊢1\cdot 31+14=45$$
87	14 42 41 72 86	gcdi	$$⊢45\gcd 31=1$$
88		eqid	$$⊢45=45$$
89	67 78	oveq12i	$$⊢2\cdot 4+3+1=8+4$$
90		8p4e12	$$⊢8+4=12$$
91	89 90	eqtri	$$⊢2\cdot 4+3+1=12$$
92		5cn	$$⊢5\in ℂ$$
93		2cn	$$⊢2\in ℂ$$
94		5t2e10	$$⊢5\cdot 2=10$$
95	92 93 94	mulcomli	$$⊢2\cdot 5=10$$
96	14 4 24 95	decsuc	$$⊢2\cdot 5+1=11$$
97	17 35 12 14 88 73 11 14 14 91 96	decma2c	$$⊢2\cdot 45+31=121$$
98	11 41 36 87 97	gcdi	$$⊢121\gcd 45=1$$
99		eqid	$$⊢121=121$$
100		eqid	$$⊢12=12$$
101	48	addridi	$$⊢4+0=4$$
102	17	dec0h	$$⊢4=04$$
103	101 102	eqtri	$$⊢4+0=04$$
104		00id	$$⊢0+0=0$$
105	80 104	oveq12i	$$⊢1\cdot 1+0+0=1+0$$
106	105 76	eqtri	$$⊢1\cdot 1+0+0=1$$
107	93	mullidi	$$⊢1\cdot 2=2$$
108	107	oveq1i	$$⊢1\cdot 2+4=2+4$$
109		4p2e6	$$⊢4+2=6$$
110	48 93 109	addcomli	$$⊢2+4=6$$
111	28	dec0h	$$⊢6=06$$
112	108 110 111	3eqtri	$$⊢1\cdot 2+4=06$$
113	14 11 4 17 100 103 14 28 4 106 112	decma2c	$$⊢1\cdot 12+4+0=16$$
114	80	oveq1i	$$⊢1\cdot 1+5=1+5$$
115		5p1e6	$$⊢5+1=6$$
116	92 75 115	addcomli	$$⊢1+5=6$$
117	114 116 111	3eqtri	$$⊢1\cdot 1+5=06$$
118	39 14 17 35 99 88 14 28 4 113 117	decma2c	$$⊢1\cdot 121+45=166$$
119	14 36 40 98 118	gcdi	$$⊢166\gcd 121=1$$
120		eqid	$$⊢166=166$$
121		eqid	$$⊢16=16$$
122	14 11 65 100	decsuc	$$⊢12+1=13$$
123		1p1e2	$$⊢1+1=2$$
124	63 123	oveq12i	$$⊢2\cdot 1+1+1=2+2$$
125	124 52	eqtri	$$⊢2\cdot 1+1+1=4$$
126		6cn	$$⊢6\in ℂ$$
127		6t2e12	$$⊢6\cdot 2=12$$
128	126 93 127	mulcomli	$$⊢2\cdot 6=12$$
129		3p2e5	$$⊢3+2=5$$
130	49 93 129	addcomli	$$⊢2+3=5$$
131	14 11 12 128 130	decaddi	$$⊢2\cdot 6+3=15$$
132	14 28 14 12 121 122 11 35 14 125 131	decma2c	$$⊢2\cdot 16+12+1=45$$
133	14 11 65 128	decsuc	$$⊢2\cdot 6+1=13$$
134	29 28 39 14 120 99 11 12 14 132 133	decma2c	$$⊢2\cdot 166+121=453$$
135	11 40 38 119 134	gcdi	$$⊢453\gcd 166=1$$
136		eqid	$$⊢453=453$$
137	29	nn0cni	$$⊢16\in ℂ$$
138	137	addridi	$$⊢16+0=16$$
139	48	mullidi	$$⊢1\cdot 4=4$$
140	139 123	oveq12i	$$⊢1\cdot 4+1+1=4+2$$
141	140 109	eqtri	$$⊢1\cdot 4+1+1=6$$
142	92	mullidi	$$⊢1\cdot 5=5$$
143	142	oveq1i	$$⊢1\cdot 5+6=5+6$$
144		6p5e11	$$⊢6+5=11$$
145	126 92 144	addcomli	$$⊢5+6=11$$
146	143 145	eqtri	$$⊢1\cdot 5+6=11$$
147	17 35 14 28 88 138 14 14 14 141 146	decma2c	$$⊢1\cdot 45+16+0=61$$
148	74	oveq1i	$$⊢1\cdot 3+6=3+6$$
149		6p3e9	$$⊢6+3=9$$
150	126 49 149	addcomli	$$⊢3+6=9$$
151	30	dec0h	$$⊢9=09$$
152	148 150 151	3eqtri	$$⊢1\cdot 3+6=09$$
153	36 12 29 28 136 120 14 30 4 147 152	decma2c	$$⊢1\cdot 453+166=619$$
154	14 38 37 135 153	gcdi	$$⊢619\gcd 453=1$$
155		eqid	$$⊢619=619$$
156		7nn0	$$⊢7\in {\mathbb{N}}_0$$
157		eqid	$$⊢61=61$$
158		5p2e7	$$⊢5+2=7$$
159	17 35 11 88 158	decaddi	$$⊢45+2=47$$
160	101	oveq2i	$$⊢2\cdot 6+4+0=2\cdot 6+4$$
161	14 11 17 128 110	decaddi	$$⊢2\cdot 6+4=16$$
162	160 161	eqtri	$$⊢2\cdot 6+4+0=16$$
163	63	oveq1i	$$⊢2\cdot 1+7=2+7$$
164		7cn	$$⊢7\in ℂ$$
165		7p2e9	$$⊢7+2=9$$
166	164 93 165	addcomli	$$⊢2+7=9$$
167	163 166 151	3eqtri	$$⊢2\cdot 1+7=09$$
168	28 14 17 156 157 159 11 30 4 162 167	decma2c	$$⊢2\cdot 61+45+2=169$$
169		9cn	$$⊢9\in ℂ$$
170		9t2e18	$$⊢9\cdot 2=18$$
171	169 93 170	mulcomli	$$⊢2\cdot 9=18$$
172	14 3 12 171 123 14 69	decaddci	$$⊢2\cdot 9+3=21$$
173	33 30 36 12 155 136 11 14 11 168 172	decma2c	$$⊢2\cdot 619+453=1691$$
174	11 37 34 154 173	gcdi	$$⊢1691\gcd 619=1$$
175		eqid	$$⊢1691=1691$$
176		eqid	$$⊢169=169$$
177	28 14 123 157	decsuc	$$⊢61+1=62$$
178		6p1e7	$$⊢6+1=7$$
179	156	dec0h	$$⊢7=07$$
180	178 179	eqtri	$$⊢6+1=07$$
181	80 24	oveq12i	$$⊢1\cdot 1+0+1=1+1$$
182	181 123	eqtri	$$⊢1\cdot 1+0+1=2$$
183	126	mullidi	$$⊢1\cdot 6=6$$
184	183	oveq1i	$$⊢1\cdot 6+7=6+7$$
185		7p6e13	$$⊢7+6=13$$
186	164 126 185	addcomli	$$⊢6+7=13$$
187	184 186	eqtri	$$⊢1\cdot 6+7=13$$
188	14 28 4 156 121 180 14 12 14 182 187	decma2c	$$⊢1\cdot 16+6+1=23$$
189	169	mullidi	$$⊢1\cdot 9=9$$
190	189	oveq1i	$$⊢1\cdot 9+2=9+2$$
191		9p2e11	$$⊢9+2=11$$
192	190 191	eqtri	$$⊢1\cdot 9+2=11$$
193	29 30 28 11 176 177 14 14 14 188 192	decma2c	$$⊢1\cdot 169+61+1=231$$
194	80	oveq1i	$$⊢1\cdot 1+9=1+9$$
195		9p1e10	$$⊢9+1=10$$
196	169 75 195	addcomli	$$⊢1+9=10$$
197	194 196	eqtri	$$⊢1\cdot 1+9=10$$
198	31 14 33 30 175 155 14 4 14 193 197	decma2c	$$⊢1\cdot 1691+619=2310$$
199	14 34 32 174 198	gcdi	$$⊢2310\gcd 1691=1$$
200		eqid	$$⊢231=231$$
201	31	nn0cni	$$⊢169\in ℂ$$
202	201	addridi	$$⊢169+0=169$$
203		eqid	$$⊢23=23$$
204	14 28 178 121	decsuc	$$⊢16+1=17$$
205	107 123	oveq12i	$$⊢1\cdot 2+1+1=2+2$$
206	205 52	eqtri	$$⊢1\cdot 2+1+1=4$$
207	74	oveq1i	$$⊢1\cdot 3+7=3+7$$
208		7p3e10	$$⊢7+3=10$$
209	164 49 208	addcomli	$$⊢3+7=10$$
210	207 209	eqtri	$$⊢1\cdot 3+7=10$$
211	11 12 14 156 203 204 14 4 14 206 210	decma2c	$$⊢1\cdot 23+16+1=40$$
212	13 14 29 30 200 202 14 4 14 211 197	decma2c	$$⊢1\cdot 231+169+0=400$$
213	75	mul01i	$$⊢1\cdot 0=0$$
214	213	oveq1i	$$⊢1\cdot 0+1=0+1$$
215	14	dec0h	$$⊢1=01$$
216	214 24 215	3eqtri	$$⊢1\cdot 0+1=01$$
217	15 4 31 14 25 175 14 14 4 212 216	decma2c	$$⊢1\cdot 2310+1691=4001$$
218	217 1	eqtr4i	$$⊢1\cdot 2310+1691=N$$
219	14 32 16 199 218	gcdi	$$⊢N\gcd 2310=1$$
220	10 16 22 27 219	gcdmodi	$$⊢\left(2^{800}-1\right)\gcd N=1$$