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