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