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		4cn	|- 4 e. CC
24		2cn	|- 2 e. CC
25	23 24 13	mulcomli	|- ( 2 x. 4 ) = 8
26	25	oveq1i	|- ( ( 2 x. 4 ) + 0 ) = ( 8 + 0 )
27		8cn	|- 8 e. CC
28	27	addid1i	|- ( 8 + 0 ) = 8
29	26 28	eqtri	|- ( ( 2 x. 4 ) + 0 ) = 8
30		2t2e4	|- ( 2 x. 2 ) = 4
31	1	dec0h	|- 4 = ; 0 4
32	31	eqcomi	|- ; 0 4 = 4
33	30 32	eqtr4i	|- ( 2 x. 2 ) = ; 0 4
34	18 1 18 22 1 20 29 33	decmul2c	|- ( 2 x. ; 4 2 ) = ; 8 4
35	23	addid1i	|- ( 4 + 0 ) = 4
36	7 1 20 34 35	decaddi	|- ( ( 2 x. ; 4 2 ) + 0 ) = ; 8 4
37		2t0e0	|- ( 2 x. 0 ) = 0
38	20	dec0h	|- 0 = ; 0 0
39	38	eqcomi	|- ; 0 0 = 0
40	37 39	eqtr4i	|- ( 2 x. 0 ) = ; 0 0
41	18 19 20 21 20 20 36 40	decmul2c	|- ( 2 x. ; ; 4 2 0 ) = ; ; 8 4 0
42	41	oveq2i	|- ( 4 x. ( 2 x. ; ; 4 2 0 ) ) = ( 4 x. ; ; 8 4 0 )
43	17 42	eqtri	|- ( ; ; 4 2 0 x. 8 ) = ( 4 x. ; ; 8 4 0 )
44	4 5 6 9 10 11 43	lcmeprodgcdi	|- ( ; ; 4 2 0 lcm 8 ) = ; ; 8 4 0