Theorem 60lcm6e60

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

	Ref	Expression
Assertion	60lcm6e60	$$⊢60\mathrm{lcm}6=60$$

Proof

Step	Hyp	Ref	Expression
1		6nn	$$⊢6\in \mathbb{N}$$
2	1	decnncl2	$$⊢60\in \mathbb{N}$$
3		60gcd6e6	$$⊢60\gcd 6=6$$
4		eqid	$$⊢6\cdot 60=6\cdot 60$$
5	2 1	mulcomnni	$$⊢60\cdot 6=6\cdot 60$$
6	2 1 1 2 3 4 5	lcmeprodgcdi	$$⊢60\mathrm{lcm}6=60$$