Theorem 60gcd6e6

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

	Ref	Expression
Assertion	60gcd6e6	⊢ ( ; 6 0 gcd 6 ) = 6

Proof

Step	Hyp	Ref	Expression
1		6nn	⊢ 6 ∈ ℕ
2	1	decnncl2	⊢ ; 6 0 ∈ ℕ
3	1 2	gcdcomnni	⊢ ( 6 gcd ; 6 0 ) = ( ; 6 0 gcd 6 )
4	1	nnnn0i	⊢ 6 ∈ ℕ0
5		1nn0	⊢ 1 ∈ ℕ0
6		0nn0	⊢ 0 ∈ ℕ0
7		eqid	⊢ ; 1 0 = ; 1 0
8		6cn	⊢ 6 ∈ ℂ
9	8	mullidi	⊢ ( 1 · 6 ) = 6
10	8	mul02i	⊢ ( 0 · 6 ) = 0
11	4 5 6 7 9 10	decmul1	⊢ ( ; 1 0 · 6 ) = ; 6 0
12		10nn	⊢ ; 1 0 ∈ ℕ
13	12 1	mulcomnni	⊢ ( ; 1 0 · 6 ) = ( 6 · ; 1 0 )
14	11 13	eqtr3i	⊢ ; 6 0 = ( 6 · ; 1 0 )
15	14	oveq2i	⊢ ( 6 gcd ; 6 0 ) = ( 6 gcd ( 6 · ; 1 0 ) )
16	1 12	gcdmultiplei	⊢ ( 6 gcd ( 6 · ; 1 0 ) ) = 6
17	15 16	eqtri	⊢ ( 6 gcd ; 6 0 ) = 6
18	3 17	eqtr3i	⊢ ( ; 6 0 gcd 6 ) = 6