Metamath Proof Explorer


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
2 1 decnncl2 60
3 1 2 gcdcomnni 6 gcd 60 = 60 gcd 6
4 1 nnnn0i 6 0
5 1nn0 1 0
6 0nn0 0 0
7 eqid 10 = 10
8 6cn 6
9 8 mulid2i 1 6 = 6
10 8 mul02i 0 6 = 0
11 4 5 6 7 9 10 decmul1 10 6 = 60
12 10nn 10
13 12 1 mulcomnni 10 6 = 6 10
14 11 13 eqtr3i 60 = 6 10
15 14 oveq2i 6 gcd 60 = 6 gcd 6 10
16 1 12 gcdmultiplei 6 gcd 6 10 = 6
17 15 16 eqtri 6 gcd 60 = 6
18 3 17 eqtr3i 60 gcd 6 = 6