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 e. NN0
2		2nn	|- 2 e. NN
3	1 2	decnncl	|- ; 1 2 e. NN
4		5nn	|- 5 e. NN
5		1nn	|- 1 e. NN
6		6nn	|- 6 e. NN
7	6	decnncl2	|- ; 6 0 e. NN
8		12gcd5e1	|- ( ; 1 2 gcd 5 ) = 1
9		6nn0	|- 6 e. NN0
10		0nn0	|- 0 e. NN0
11	9 10	deccl	|- ; 6 0 e. NN0
12	11	nn0cni	|- ; 6 0 e. CC
13	12	mulid2i	|- ( 1 x. ; 6 0 ) = ; 6 0
14		5nn0	|- 5 e. NN0
15		2nn0	|- 2 e. NN0
16		eqid	|- ; 1 2 = ; 1 2
17		5cn	|- 5 e. CC
18	17	mulid2i	|- ( 1 x. 5 ) = 5
19	18	oveq1i	|- ( ( 1 x. 5 ) + 1 ) = ( 5 + 1 )
20		5p1e6	|- ( 5 + 1 ) = 6
21	19 20	eqtri	|- ( ( 1 x. 5 ) + 1 ) = 6
22		2cn	|- 2 e. CC
23		5t2e10	|- ( 5 x. 2 ) = ; 1 0
24	17 22 23	mulcomli	|- ( 2 x. 5 ) = ; 1 0
25	14 1 15 16 10 1 21 24	decmul1c	|- ( ; 1 2 x. 5 ) = ; 6 0
26	3 4 5 7 8 13 25	lcmeprodgcdi	|- ( ; 1 2 lcm 5 ) = ; 6 0