Theorem 12lcm5e60

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

	Ref	Expression
Assertion	12lcm5e60	⊢ ( ; 1 2 lcm 5 ) = ; 6 0

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		2nn	⊢ 2 ∈ ℕ
3	1 2	decnncl	⊢ ; 1 2 ∈ ℕ
4		5nn	⊢ 5 ∈ ℕ
5		1nn	⊢ 1 ∈ ℕ
6		6nn	⊢ 6 ∈ ℕ
7	6	decnncl2	⊢ ; 6 0 ∈ ℕ
8		12gcd5e1	⊢ ( ; 1 2 gcd 5 ) = 1
9		6nn0	⊢ 6 ∈ ℕ0
10		0nn0	⊢ 0 ∈ ℕ0
11	9 10	deccl	⊢ ; 6 0 ∈ ℕ0
12	11	nn0cni	⊢ ; 6 0 ∈ ℂ
13	12	mulid2i	⊢ ( 1 · ; 6 0 ) = ; 6 0
14		5nn0	⊢ 5 ∈ ℕ0
15		2nn0	⊢ 2 ∈ ℕ0
16		eqid	⊢ ; 1 2 = ; 1 2
17		5cn	⊢ 5 ∈ ℂ
18	17	mulid2i	⊢ ( 1 · 5 ) = 5
19	18	oveq1i	⊢ ( ( 1 · 5 ) + 1 ) = ( 5 + 1 )
20		5p1e6	⊢ ( 5 + 1 ) = 6
21	19 20	eqtri	⊢ ( ( 1 · 5 ) + 1 ) = 6
22		2cn	⊢ 2 ∈ ℂ
23		5t2e10	⊢ ( 5 · 2 ) = ; 1 0
24	17 22 23	mulcomli	⊢ ( 2 · 5 ) = ; 1 0
25	14 1 15 16 10 1 21 24	decmul1c	⊢ ( ; 1 2 · 5 ) = ; 6 0
26	3 4 5 7 8 13 25	lcmeprodgcdi	⊢ ( ; 1 2 lcm 5 ) = ; 6 0