Metamath Proof Explorer


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 mulid2i ( 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