Theorem 60lcm6e60

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

	Ref	Expression
Assertion	60lcm6e60	⊢ ( ; 6 0 lcm 6 ) = ; 6 0

Proof

Step	Hyp	Ref	Expression
1		6nn	⊢ 6 ∈ ℕ
2	1	decnncl2	⊢ ; 6 0 ∈ ℕ
3		60gcd6e6	⊢ ( ; 6 0 gcd 6 ) = 6
4		eqid	⊢ ( 6 · ; 6 0 ) = ( 6 · ; 6 0 )
5	2 1	mulcomnni	⊢ ( ; 6 0 · 6 ) = ( 6 · ; 6 0 )
6	2 1 1 2 3 4 5	lcmeprodgcdi	⊢ ( ; 6 0 lcm 6 ) = ; 6 0