Theorem 60gcd6e6

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

	Ref	Expression
Assertion	60gcd6e6	$$⊢60\gcd 6=6$$

Proof

Step	Hyp	Ref	Expression
1		6nn	$$⊢6\in \mathbb{N}$$
2	1	decnncl2	$$⊢60\in \mathbb{N}$$
3	1 2	gcdcomnni	$$⊢6\gcd 60=60\gcd 6$$
4	1	nnnn0i	$$⊢6\in {\mathbb{N}}_0$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7		eqid	$$⊢10=10$$
8		6cn	$$⊢6\in ℂ$$
9	8	mulid2i	$$⊢1\cdot 6=6$$
10	8	mul02i	$$⊢0\cdot 6=0$$
11	4 5 6 7 9 10	decmul1	$$⊢10\cdot 6=60$$
12		10nn	$$⊢10\in \mathbb{N}$$
13	12 1	mulcomnni	$$⊢10\cdot 6=6\cdot 10$$
14	11 13	eqtr3i	$$⊢60=6\cdot 10$$
15	14	oveq2i	$$⊢6\gcd 60=6\gcd 6\cdot 10$$
16	1 12	gcdmultiplei	$$⊢6\gcd 6\cdot 10=6$$
17	15 16	eqtri	$$⊢6\gcd 60=6$$
18	3 17	eqtr3i	$$⊢60\gcd 6=6$$