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 ∈ ℕ0
2		2nn	⊢ 2 ∈ ℕ
3	1 2	decnncl	⊢ ; 4 2 ∈ ℕ
4	3	decnncl2	⊢ ; ; 4 2 0 ∈ ℕ
5		8nn	⊢ 8 ∈ ℕ
6		4nn	⊢ 4 ∈ ℕ
7		8nn0	⊢ 8 ∈ ℕ0
8	7 6	decnncl	⊢ ; 8 4 ∈ ℕ
9	8	decnncl2	⊢ ; ; 8 4 0 ∈ ℕ
10		420gcd8e4	⊢ ( ; ; 4 2 0 gcd 8 ) = 4
11		eqid	⊢ ( 4 · ; ; 8 4 0 ) = ( 4 · ; ; 8 4 0 )
12	4 5	mulcomnni	⊢ ( ; ; 4 2 0 · 8 ) = ( 8 · ; ; 4 2 0 )
13		4t2e8	⊢ ( 4 · 2 ) = 8
14	13	oveq1i	⊢ ( ( 4 · 2 ) · ; ; 4 2 0 ) = ( 8 · ; ; 4 2 0 )
15	12 14	eqtr4i	⊢ ( ; ; 4 2 0 · 8 ) = ( ( 4 · 2 ) · ; ; 4 2 0 )
16	6 2 4	mulassnni	⊢ ( ( 4 · 2 ) · ; ; 4 2 0 ) = ( 4 · ( 2 · ; ; 4 2 0 ) )
17	15 16	eqtri	⊢ ( ; ; 4 2 0 · 8 ) = ( 4 · ( 2 · ; ; 4 2 0 ) )
18	2	nnnn0i	⊢ 2 ∈ ℕ0
19	3	nnnn0i	⊢ ; 4 2 ∈ ℕ0
20		0nn0	⊢ 0 ∈ ℕ0
21		eqid	⊢ ; ; 4 2 0 = ; ; 4 2 0
22		eqid	⊢ ; 4 2 = ; 4 2
23		2t4e8	⊢ ( 2 · 4 ) = 8
24	23	oveq1i	⊢ ( ( 2 · 4 ) + 0 ) = ( 8 + 0 )
25		8cn	⊢ 8 ∈ ℂ
26	25	addridi	⊢ ( 8 + 0 ) = 8
27	24 26	eqtri	⊢ ( ( 2 · 4 ) + 0 ) = 8
28		2t2e4	⊢ ( 2 · 2 ) = 4
29	1	dec0h	⊢ 4 = ; 0 4
30	29	eqcomi	⊢ ; 0 4 = 4
31	28 30	eqtr4i	⊢ ( 2 · 2 ) = ; 0 4
32	18 1 18 22 1 20 27 31	decmul2c	⊢ ( 2 · ; 4 2 ) = ; 8 4
33		4cn	⊢ 4 ∈ ℂ
34	33	addridi	⊢ ( 4 + 0 ) = 4
35	7 1 20 32 34	decaddi	⊢ ( ( 2 · ; 4 2 ) + 0 ) = ; 8 4
36		2t0e0	⊢ ( 2 · 0 ) = 0
37	20	dec0h	⊢ 0 = ; 0 0
38	37	eqcomi	⊢ ; 0 0 = 0
39	36 38	eqtr4i	⊢ ( 2 · 0 ) = ; 0 0
40	18 19 20 21 20 20 35 39	decmul2c	⊢ ( 2 · ; ; 4 2 0 ) = ; ; 8 4 0
41	40	oveq2i	⊢ ( 4 · ( 2 · ; ; 4 2 0 ) ) = ( 4 · ; ; 8 4 0 )
42	17 41	eqtri	⊢ ( ; ; 4 2 0 · 8 ) = ( 4 · ; ; 8 4 0 )
43	4 5 6 9 10 11 42	lcmeprodgcdi	⊢ ( ; ; 4 2 0 lcm 8 ) = ; ; 8 4 0