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