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		4cn	$$⊢4\in ℂ$$
89		4t2e8	$$⊢4\cdot 2=8$$
90	88 69 89	mulcomli	$$⊢2\cdot 4=8$$
91	90	oveq1i	$$⊢2\cdot 4+1=8+1$$
92		8p1e9	$$⊢8+1=9$$
93	13	dec0h	$$⊢9=09$$
94	91 92 93	3eqtri	$$⊢2\cdot 4+1=09$$
95	3 4 16 15 82 68 16 13 31 87 94	decma2c	$$⊢2\cdot 34+21=89$$
96	16 34 5 81 95	gcdi	$$⊢89\gcd 34=1$$
97		eqid	$$⊢89=89$$
98		4p3e7	$$⊢4+3=7$$
99	88 51 98	addcomli	$$⊢3+4=7$$
100	99	oveq2i	$$⊢4\cdot 8+3+4=4\cdot 8+7$$
101		7nn0	$$⊢7\in {\mathbb{N}}_0$$
102		8t4e32	$$⊢8\cdot 4=32$$
103	54 88 102	mulcomli	$$⊢4\cdot 8=32$$
104		7cn	$$⊢7\in ℂ$$
105		7p2e9	$$⊢7+2=9$$
106	104 69 105	addcomli	$$⊢2+7=9$$
107	3 16 101 103 106	decaddi	$$⊢4\cdot 8+7=39$$
108	100 107	eqtri	$$⊢4\cdot 8+3+4=39$$
109		9cn	$$⊢9\in ℂ$$
110		9t4e36	$$⊢9\cdot 4=36$$
111	109 88 110	mulcomli	$$⊢4\cdot 9=36$$
112		6p4e10	$$⊢6+4=10$$
113	3 11 4 111 76 112	decaddci2	$$⊢4\cdot 9+4=40$$
114	10 13 3 4 97 82 4 31 4 108 113	decma2c	$$⊢4\cdot 89+34=390$$
115	4 5 33 96 114	gcdi	$$⊢390\gcd 89=1$$
116		eqid	$$⊢390=390$$
117		eqid	$$⊢39=39$$
118	54	addridi	$$⊢8+0=8$$
119	118 44	eqtri	$$⊢8+0=08$$
120	69	addlidi	$$⊢0+2=2$$
121	83 120	oveq12i	$$⊢2\cdot 3+0+2=6+2$$
122	121 86	eqtri	$$⊢2\cdot 3+0+2=8$$
123		9t2e18	$$⊢9\cdot 2=18$$
124	109 69 123	mulcomli	$$⊢2\cdot 9=18$$
125		8p8e16	$$⊢8+8=16$$
126	15 10 10 124 49 11 125	decaddci	$$⊢2\cdot 9+8=26$$
127	3 13 31 10 117 119 16 11 16 122 126	decma2c	$$⊢2\cdot 39+8+0=86$$
128		2t0e0	$$⊢2\cdot 0=0$$
129	128	oveq1i	$$⊢2\cdot 0+9=0+9$$
130	109	addlidi	$$⊢0+9=9$$
131	129 130 93	3eqtri	$$⊢2\cdot 0+9=09$$
132	30 31 10 13 116 97 16 13 31 127 131	decma2c	$$⊢2\cdot 390+89=869$$
133	16 33 32 115 132	gcdi	$$⊢869\gcd 390=1$$
134	30	nn0cni	$$⊢39\in ℂ$$
135	134	addridi	$$⊢39+0=39$$
136	54	mullidi	$$⊢1\cdot 8=8$$
137	136 76	oveq12i	$$⊢1\cdot 8+3+1=8+4$$
138		8p4e12	$$⊢8+4=12$$
139	137 138	eqtri	$$⊢1\cdot 8+3+1=12$$
140		6cn	$$⊢6\in ℂ$$
141	140	mullidi	$$⊢1\cdot 6=6$$
142	141	oveq1i	$$⊢1\cdot 6+9=6+9$$
143		9p6e15	$$⊢9+6=15$$
144	109 140 143	addcomli	$$⊢6+9=15$$
145	142 144	eqtri	$$⊢1\cdot 6+9=15$$
146	10 11 3 13 25 135 15 18 15 139 145	decma2c	$$⊢1\cdot 86+39+0=125$$
147	109	mullidi	$$⊢1\cdot 9=9$$
148	147	oveq1i	$$⊢1\cdot 9+0=9+0$$
149	109	addridi	$$⊢9+0=9$$
150	148 149 93	3eqtri	$$⊢1\cdot 9+0=09$$
151	12 13 30 31 27 116 15 13 31 146 150	decma2c	$$⊢1\cdot 869+390=1259$$
152	151 1	eqtr4i	$$⊢1\cdot 869+390=N$$
153	15 32 14 133 152	gcdi	$$⊢N\gcd 869=1$$
154	9 14 22 29 153	gcdmodi	$$⊢\left(2^{34}-1\right)\gcd N=1$$