Theorem 1259lem5

Description: Lemma for 1259prm . Calculate the GCD of 2 ^ 3 4 - 1 == 8 6 9 with N = 1 2 5 9 . (Contributed by Mario Carneiro, 22-Feb-2014) (Revised by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Hypothesis	1259prm.1	$$⊢N=1259$$
Assertion	1259lem5	$$⊢\left(2^{34}-1\right)\gcd N=1$$

Proof

Step	Hyp	Ref	Expression
1		1259prm.1	$$⊢N=1259$$
2		2nn	$$⊢2\in \mathbb{N}$$
3		3nn0	$$⊢3\in {\mathbb{N}}_0$$
4		4nn0	$$⊢4\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢34\in {\mathbb{N}}_0$$
6		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge 34\in {\mathbb{N}}_0\right)\to 2^{34}\in \mathbb{N}$$
7	2 5 6	mp2an	$$⊢2^{34}\in \mathbb{N}$$
8		nnm1nn0	$$⊢2^{34}\in \mathbb{N}\to 2^{34}-1\in {\mathbb{N}}_0$$
9	7 8	ax-mp	$$⊢2^{34}-1\in {\mathbb{N}}_0$$
10		8nn0	$$⊢8\in {\mathbb{N}}_0$$
11		6nn0	$$⊢6\in {\mathbb{N}}_0$$
12	10 11	deccl	$$⊢86\in {\mathbb{N}}_0$$
13		9nn0	$$⊢9\in {\mathbb{N}}_0$$
14	12 13	deccl	$$⊢869\in {\mathbb{N}}_0$$
15		1nn0	$$⊢1\in {\mathbb{N}}_0$$
16		2nn0	$$⊢2\in {\mathbb{N}}_0$$
17	15 16	deccl	$$⊢12\in {\mathbb{N}}_0$$
18		5nn0	$$⊢5\in {\mathbb{N}}_0$$
19	17 18	deccl	$$⊢125\in {\mathbb{N}}_0$$
20		9nn	$$⊢9\in \mathbb{N}$$
21	19 20	decnncl	$$⊢1259\in \mathbb{N}$$
22	1 21	eqeltri	$$⊢N\in \mathbb{N}$$
23	1	1259lem2	$$⊢2^{34}\mathrm{mod}N=870\mathrm{mod}N$$
24		6p1e7	$$⊢6+1=7$$
25		eqid	$$⊢86=86$$
26	10 11 24 25	decsuc	$$⊢86+1=87$$
27		eqid	$$⊢869=869$$
28	12 26 27	decsucc	$$⊢869+1=870$$
29	22 7 15 14 23 28	modsubi	$$⊢\left(2^{34}-1\right)\mathrm{mod}N=869\mathrm{mod}N$$
30	3 13	deccl	$$⊢39\in {\mathbb{N}}_0$$
31		0nn0	$$⊢0\in {\mathbb{N}}_0$$
32	30 31	deccl	$$⊢390\in {\mathbb{N}}_0$$
33	10 13	deccl	$$⊢89\in {\mathbb{N}}_0$$
34	16 15	deccl	$$⊢21\in {\mathbb{N}}_0$$
35	15 3	deccl	$$⊢13\in {\mathbb{N}}_0$$
36	34	nn0zi	$$⊢21\in \mathbb{Z}$$
37	35	nn0zi	$$⊢13\in \mathbb{Z}$$
38		gcdcom	$$⊢\left(21\in \mathbb{Z}\wedge 13\in \mathbb{Z}\right)\to 21\gcd 13=13\gcd 21$$
39	36 37 38	mp2an	$$⊢21\gcd 13=13\gcd 21$$
40		3nn	$$⊢3\in \mathbb{N}$$
41	15 40	decnncl	$$⊢13\in \mathbb{N}$$
42		8nn	$$⊢8\in \mathbb{N}$$
43		eqid	$$⊢13=13$$
44	10	dec0h	$$⊢8=08$$
45		ax-1cn	$$⊢1\in ℂ$$
46	45	mulridi	$$⊢1\cdot 1=1$$
47	45	addlidi	$$⊢0+1=1$$
48	46 47	oveq12i	$$⊢1\cdot 1+0+1=1+1$$
49		1p1e2	$$⊢1+1=2$$
50	48 49	eqtri	$$⊢1\cdot 1+0+1=2$$
51		3cn	$$⊢3\in ℂ$$
52	51	mulridi	$$⊢3\cdot 1=3$$
53	52	oveq1i	$$⊢3\cdot 1+8=3+8$$
54		8cn	$$⊢8\in ℂ$$
55		8p3e11	$$⊢8+3=11$$
56	54 51 55	addcomli	$$⊢3+8=11$$
57	53 56	eqtri	$$⊢3\cdot 1+8=11$$
58	15 3 31 10 43 44 15 15 15 50 57	decmac	$$⊢13\cdot 1+8=21$$
59		1nn	$$⊢1\in \mathbb{N}$$
60		8lt10	$$⊢8<10$$
61	59 3 10 60	declti	$$⊢8<13$$
62	41 15 42 58 61	ndvdsi	$$⊢\neg 13\parallel 21$$
63		13prm	$$⊢13\in \mathbb{P}$$
64		coprm	$$⊢\left(13\in \mathbb{P}\wedge 21\in \mathbb{Z}\right)\to \left(\neg 13\parallel 21\leftrightarrow 13\gcd 21=1\right)$$
65	63 36 64	mp2an	$$⊢\neg 13\parallel 21\leftrightarrow 13\gcd 21=1$$
66	62 65	mpbi	$$⊢13\gcd 21=1$$
67	39 66	eqtri	$$⊢21\gcd 13=1$$
68		eqid	$$⊢21=21$$
69		2cn	$$⊢2\in ℂ$$
70	69	mullidi	$$⊢1\cdot 2=2$$
71	45	addridi	$$⊢1+0=1$$
72	70 71	oveq12i	$$⊢1\cdot 2+1+0=2+1$$
73		2p1e3	$$⊢2+1=3$$
74	72 73	eqtri	$$⊢1\cdot 2+1+0=3$$
75	46	oveq1i	$$⊢1\cdot 1+3=1+3$$
76		3p1e4	$$⊢3+1=4$$
77	51 45 76	addcomli	$$⊢1+3=4$$
78	4	dec0h	$$⊢4=04$$
79	75 77 78	3eqtri	$$⊢1\cdot 1+3=04$$
80	16 15 15 3 68 43 15 4 31 74 79	decma2c	$$⊢1\cdot 21+13=34$$
81	15 35 34 67 80	gcdi	$$⊢34\gcd 21=1$$
82		eqid	$$⊢34=34$$
83		2t3e6	$$⊢2\cdot 3=6$$
84	69	addridi	$$⊢2+0=2$$
85	83 84	oveq12i	$$⊢2\cdot 3+2+0=6+2$$
86		6p2e8	$$⊢6+2=8$$
87	85 86	eqtri	$$⊢2\cdot 3+2+0=8$$
88		2t4e8	$$⊢2\cdot 4=8$$
89	88	oveq1i	$$⊢2\cdot 4+1=8+1$$
90		8p1e9	$$⊢8+1=9$$
91	13	dec0h	$$⊢9=09$$
92	89 90 91	3eqtri	$$⊢2\cdot 4+1=09$$
93	3 4 16 15 82 68 16 13 31 87 92	decma2c	$$⊢2\cdot 34+21=89$$
94	16 34 5 81 93	gcdi	$$⊢89\gcd 34=1$$
95		eqid	$$⊢89=89$$
96		4cn	$$⊢4\in ℂ$$
97		4p3e7	$$⊢4+3=7$$
98	96 51 97	addcomli	$$⊢3+4=7$$
99	98	oveq2i	$$⊢4\cdot 8+3+4=4\cdot 8+7$$
100		7nn0	$$⊢7\in {\mathbb{N}}_0$$
101		8t4e32	$$⊢8\cdot 4=32$$
102	54 96 101	mulcomli	$$⊢4\cdot 8=32$$
103		7cn	$$⊢7\in ℂ$$
104		7p2e9	$$⊢7+2=9$$
105	103 69 104	addcomli	$$⊢2+7=9$$
106	3 16 100 102 105	decaddi	$$⊢4\cdot 8+7=39$$
107	99 106	eqtri	$$⊢4\cdot 8+3+4=39$$
108		9cn	$$⊢9\in ℂ$$
109		9t4e36	$$⊢9\cdot 4=36$$
110	108 96 109	mulcomli	$$⊢4\cdot 9=36$$
111		6p4e10	$$⊢6+4=10$$
112	3 11 4 110 76 111	decaddci2	$$⊢4\cdot 9+4=40$$
113	10 13 3 4 95 82 4 31 4 107 112	decma2c	$$⊢4\cdot 89+34=390$$
114	4 5 33 94 113	gcdi	$$⊢390\gcd 89=1$$
115		eqid	$$⊢390=390$$
116		eqid	$$⊢39=39$$
117	54	addridi	$$⊢8+0=8$$
118	117 44	eqtri	$$⊢8+0=08$$
119	69	addlidi	$$⊢0+2=2$$
120	83 119	oveq12i	$$⊢2\cdot 3+0+2=6+2$$
121	120 86	eqtri	$$⊢2\cdot 3+0+2=8$$
122		9t2e18	$$⊢9\cdot 2=18$$
123	108 69 122	mulcomli	$$⊢2\cdot 9=18$$
124		8p8e16	$$⊢8+8=16$$
125	15 10 10 123 49 11 124	decaddci	$$⊢2\cdot 9+8=26$$
126	3 13 31 10 116 118 16 11 16 121 125	decma2c	$$⊢2\cdot 39+8+0=86$$
127		2t0e0	$$⊢2\cdot 0=0$$
128	127	oveq1i	$$⊢2\cdot 0+9=0+9$$
129	108	addlidi	$$⊢0+9=9$$
130	128 129 91	3eqtri	$$⊢2\cdot 0+9=09$$
131	30 31 10 13 115 95 16 13 31 126 130	decma2c	$$⊢2\cdot 390+89=869$$
132	16 33 32 114 131	gcdi	$$⊢869\gcd 390=1$$
133	30	nn0cni	$$⊢39\in ℂ$$
134	133	addridi	$$⊢39+0=39$$
135	54	mullidi	$$⊢1\cdot 8=8$$
136	135 76	oveq12i	$$⊢1\cdot 8+3+1=8+4$$
137		8p4e12	$$⊢8+4=12$$
138	136 137	eqtri	$$⊢1\cdot 8+3+1=12$$
139		6cn	$$⊢6\in ℂ$$
140	139	mullidi	$$⊢1\cdot 6=6$$
141	140	oveq1i	$$⊢1\cdot 6+9=6+9$$
142		9p6e15	$$⊢9+6=15$$
143	108 139 142	addcomli	$$⊢6+9=15$$
144	141 143	eqtri	$$⊢1\cdot 6+9=15$$
145	10 11 3 13 25 134 15 18 15 138 144	decma2c	$$⊢1\cdot 86+39+0=125$$
146	108	mullidi	$$⊢1\cdot 9=9$$
147	146	oveq1i	$$⊢1\cdot 9+0=9+0$$
148	108	addridi	$$⊢9+0=9$$
149	147 148 91	3eqtri	$$⊢1\cdot 9+0=09$$
150	12 13 30 31 27 115 15 13 31 145 149	decma2c	$$⊢1\cdot 869+390=1259$$
151	150 1	eqtr4i	$$⊢1\cdot 869+390=N$$
152	15 32 14 132 151	gcdi	$$⊢N\gcd 869=1$$
153	9 14 22 29 152	gcdmodi	$$⊢\left(2^{34}-1\right)\gcd N=1$$