Theorem 12lcm5e60

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

	Ref	Expression
Assertion	12lcm5e60	$$⊢12\mathrm{lcm}5=60$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		2nn	$$⊢2\in \mathbb{N}$$
3	1 2	decnncl	$$⊢12\in \mathbb{N}$$
4		5nn	$$⊢5\in \mathbb{N}$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		6nn	$$⊢6\in \mathbb{N}$$
7	6	decnncl2	$$⊢60\in \mathbb{N}$$
8		12gcd5e1	$$⊢12\gcd 5=1$$
9		6nn0	$$⊢6\in {\mathbb{N}}_0$$
10		0nn0	$$⊢0\in {\mathbb{N}}_0$$
11	9 10	deccl	$$⊢60\in {\mathbb{N}}_0$$
12	11	nn0cni	$$⊢60\in ℂ$$
13	12	mulid2i	$$⊢1\cdot 60=60$$
14		5nn0	$$⊢5\in {\mathbb{N}}_0$$
15		2nn0	$$⊢2\in {\mathbb{N}}_0$$
16		eqid	$$⊢12=12$$
17		5cn	$$⊢5\in ℂ$$
18	17	mulid2i	$$⊢1\cdot 5=5$$
19	18	oveq1i	$$⊢1\cdot 5+1=5+1$$
20		5p1e6	$$⊢5+1=6$$
21	19 20	eqtri	$$⊢1\cdot 5+1=6$$
22		2cn	$$⊢2\in ℂ$$
23		5t2e10	$$⊢5\cdot 2=10$$
24	17 22 23	mulcomli	$$⊢2\cdot 5=10$$
25	14 1 15 16 10 1 21 24	decmul1c	$$⊢12\cdot 5=60$$
26	3 4 5 7 8 13 25	lcmeprodgcdi	$$⊢12\mathrm{lcm}5=60$$