Theorem 420lcm8e840

Description: The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Assertion	420lcm8e840	|- ( ; ; 4 2 0 lcm 8 ) = ; ; 8 4 0

Proof

Step	Hyp	Ref	Expression
1		4nn0	|- 4 e. NN0
2		2nn	|- 2 e. NN
3	1 2	decnncl	|- ; 4 2 e. NN
4	3	decnncl2	|- ; ; 4 2 0 e. NN
5		8nn	|- 8 e. NN
6		4nn	|- 4 e. NN
7		8nn0	|- 8 e. NN0
8	7 6	decnncl	|- ; 8 4 e. NN
9	8	decnncl2	|- ; ; 8 4 0 e. NN
10		420gcd8e4	|- ( ; ; 4 2 0 gcd 8 ) = 4
11		eqid	|- ( 4 x. ; ; 8 4 0 ) = ( 4 x. ; ; 8 4 0 )
12	4 5	mulcomnni	|- ( ; ; 4 2 0 x. 8 ) = ( 8 x. ; ; 4 2 0 )
13		4t2e8	|- ( 4 x. 2 ) = 8
14	13	oveq1i	|- ( ( 4 x. 2 ) x. ; ; 4 2 0 ) = ( 8 x. ; ; 4 2 0 )
15	12 14	eqtr4i	|- ( ; ; 4 2 0 x. 8 ) = ( ( 4 x. 2 ) x. ; ; 4 2 0 )
16	6 2 4	mulassnni	|- ( ( 4 x. 2 ) x. ; ; 4 2 0 ) = ( 4 x. ( 2 x. ; ; 4 2 0 ) )
17	15 16	eqtri	|- ( ; ; 4 2 0 x. 8 ) = ( 4 x. ( 2 x. ; ; 4 2 0 ) )
18	2	nnnn0i	|- 2 e. NN0
19	3	nnnn0i	|- ; 4 2 e. NN0
20		0nn0	|- 0 e. NN0
21		eqid	|- ; ; 4 2 0 = ; ; 4 2 0
22		eqid	|- ; 4 2 = ; 4 2
23		2t4e8	|- ( 2 x. 4 ) = 8
24	23	oveq1i	|- ( ( 2 x. 4 ) + 0 ) = ( 8 + 0 )
25		8cn	|- 8 e. CC
26	25	addridi	|- ( 8 + 0 ) = 8
27	24 26	eqtri	|- ( ( 2 x. 4 ) + 0 ) = 8
28		2t2e4	|- ( 2 x. 2 ) = 4
29	1	dec0h	|- 4 = ; 0 4
30	29	eqcomi	|- ; 0 4 = 4
31	28 30	eqtr4i	|- ( 2 x. 2 ) = ; 0 4
32	18 1 18 22 1 20 27 31	decmul2c	|- ( 2 x. ; 4 2 ) = ; 8 4
33		4cn	|- 4 e. CC
34	33	addridi	|- ( 4 + 0 ) = 4
35	7 1 20 32 34	decaddi	|- ( ( 2 x. ; 4 2 ) + 0 ) = ; 8 4
36		2t0e0	|- ( 2 x. 0 ) = 0
37	20	dec0h	|- 0 = ; 0 0
38	37	eqcomi	|- ; 0 0 = 0
39	36 38	eqtr4i	|- ( 2 x. 0 ) = ; 0 0
40	18 19 20 21 20 20 35 39	decmul2c	|- ( 2 x. ; ; 4 2 0 ) = ; ; 8 4 0
41	40	oveq2i	|- ( 4 x. ( 2 x. ; ; 4 2 0 ) ) = ( 4 x. ; ; 8 4 0 )
42	17 41	eqtri	|- ( ; ; 4 2 0 x. 8 ) = ( 4 x. ; ; 8 4 0 )
43	4 5 6 9 10 11 42	lcmeprodgcdi	|- ( ; ; 4 2 0 lcm 8 ) = ; ; 8 4 0