Theorem 60gcd7e1

Description: The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Assertion	60gcd7e1	$$⊢60\gcd 7=1$$

Proof

Step	Hyp	Ref	Expression
1		7nn	$$⊢7\in \mathbb{N}$$
2		6nn	$$⊢6\in \mathbb{N}$$
3	2	decnncl2	$$⊢60\in \mathbb{N}$$
4	1 3	gcdcomnni	$$⊢7\gcd 60=60\gcd 7$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		1nn	$$⊢1\in \mathbb{N}$$
7	5 6	decnncl	$$⊢11\in \mathbb{N}$$
8	1	nnzi	$$⊢7\in \mathbb{Z}$$
9	1 7 8	gcdaddmzz2nni	$$⊢7\gcd 11=7\gcd \left(11+7\cdot 7\right)$$
10		7t7e49	$$⊢7\cdot 7=49$$
11	10	oveq2i	$$⊢11+7\cdot 7=11+49$$
12		4nn0	$$⊢4\in {\mathbb{N}}_0$$
13		9nn0	$$⊢9\in {\mathbb{N}}_0$$
14		eqid	$$⊢11=11$$
15		eqid	$$⊢49=49$$
16		4cn	$$⊢4\in ℂ$$
17		ax-1cn	$$⊢1\in ℂ$$
18		4p1e5	$$⊢4+1=5$$
19	16 17 18	addcomli	$$⊢1+4=5$$
20	19	oveq1i	$$⊢1+4+1=5+1$$
21		5p1e6	$$⊢5+1=6$$
22	20 21	eqtri	$$⊢1+4+1=6$$
23		9cn	$$⊢9\in ℂ$$
24		9p1e10	$$⊢9+1=10$$
25	23 17 24	addcomli	$$⊢1+9=10$$
26	5 5 12 13 14 15 22 25	decaddc2	$$⊢11+49=60$$
27	11 26	eqtri	$$⊢11+7\cdot 7=60$$
28	27	oveq2i	$$⊢7\gcd \left(11+7\cdot 7\right)=7\gcd 60$$
29	9 28	eqtri	$$⊢7\gcd 11=7\gcd 60$$
30		7re	$$⊢7\in ℝ$$
31	1	nnnn0i	$$⊢7\in {\mathbb{N}}_0$$
32	31	dec0h	$$⊢7=07$$
33		0nn0	$$⊢0\in {\mathbb{N}}_0$$
34		7lt9	$$⊢7<9$$
35		9re	$$⊢9\in ℝ$$
36	30 35	pm3.2i	$$⊢\left(7\in ℝ\wedge 9\in ℝ\right)$$
37		ltle	$$⊢\left(7\in ℝ\wedge 9\in ℝ\right)\to \left(7<9\to 7\le 9\right)$$
38	36 37	ax-mp	$$⊢7<9\to 7\le 9$$
39	34 38	ax-mp	$$⊢7\le 9$$
40		0lt1	$$⊢0<1$$
41	33 5 31 5 39 40	declth	$$⊢07<11$$
42	32 41	eqbrtri	$$⊢7<11$$
43		ltne	$$⊢\left(7\in ℝ\wedge 7<11\right)\to 11\ne 7$$
44	30 42 43	mp2an	$$⊢11\ne 7$$
45		necom	$$⊢7\ne 11\leftrightarrow 11\ne 7$$
46	44 45	mpbir	$$⊢7\ne 11$$
47		7prm	$$⊢7\in \mathbb{P}$$
48		11prm	$$⊢11\in \mathbb{P}$$
49		prmrp	$$⊢\left(7\in \mathbb{P}\wedge 11\in \mathbb{P}\right)\to \left(7\gcd 11=1\leftrightarrow 7\ne 11\right)$$
50	47 48 49	mp2an	$$⊢7\gcd 11=1\leftrightarrow 7\ne 11$$
51	46 50	mpbir	$$⊢7\gcd 11=1$$
52	29 51	eqtr3i	$$⊢7\gcd 60=1$$
53	4 52	eqtr3i	$$⊢60\gcd 7=1$$