Theorem 420lcm8e840

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

	Ref	Expression
Assertion	420lcm8e840	$$⊢420\mathrm{lcm}8=840$$

Proof

Step	Hyp	Ref	Expression
1		4nn0	$$⊢4\in {\mathbb{N}}_0$$
2		2nn	$$⊢2\in \mathbb{N}$$
3	1 2	decnncl	$$⊢42\in \mathbb{N}$$
4	3	decnncl2	$$⊢420\in \mathbb{N}$$
5		8nn	$$⊢8\in \mathbb{N}$$
6		4nn	$$⊢4\in \mathbb{N}$$
7		8nn0	$$⊢8\in {\mathbb{N}}_0$$
8	7 6	decnncl	$$⊢84\in \mathbb{N}$$
9	8	decnncl2	$$⊢840\in \mathbb{N}$$
10		420gcd8e4	$$⊢420\gcd 8=4$$
11		eqid	$$⊢4\cdot 840=4\cdot 840$$
12	4 5	mulcomnni	$$⊢420\cdot 8=8\cdot 420$$
13		4t2e8	$$⊢4\cdot 2=8$$
14	13	oveq1i	$$⊢4\cdot 2\cdot 420=8\cdot 420$$
15	12 14	eqtr4i	$$⊢420\cdot 8=4\cdot 2\cdot 420$$
16	6 2 4	mulassnni	$$⊢4\cdot 2\cdot 420=42\cdot 420$$
17	15 16	eqtri	$$⊢420\cdot 8=42\cdot 420$$
18	2	nnnn0i	$$⊢2\in {\mathbb{N}}_0$$
19	3	nnnn0i	$$⊢42\in {\mathbb{N}}_0$$
20		0nn0	$$⊢0\in {\mathbb{N}}_0$$
21		eqid	$$⊢420=420$$
22		eqid	$$⊢42=42$$
23		2t4e8	$$⊢2\cdot 4=8$$
24	23	oveq1i	$$⊢2\cdot 4+0=8+0$$
25		8cn	$$⊢8\in ℂ$$
26	25	addridi	$$⊢8+0=8$$
27	24 26	eqtri	$$⊢2\cdot 4+0=8$$
28		2t2e4	$$⊢2\cdot 2=4$$
29	1	dec0h	$$⊢4=04$$
30	29	eqcomi	$$⊢04=4$$
31	28 30	eqtr4i	$$⊢2\cdot 2=04$$
32	18 1 18 22 1 20 27 31	decmul2c	$$⊢2\cdot 42=84$$
33		4cn	$$⊢4\in ℂ$$
34	33	addridi	$$⊢4+0=4$$
35	7 1 20 32 34	decaddi	$$⊢2\cdot 42+0=84$$
36		2t0e0	$$⊢2\cdot 0=0$$
37	20	dec0h	$$⊢0=00$$
38	37	eqcomi	$$⊢00=0$$
39	36 38	eqtr4i	$$⊢2\cdot 0=00$$
40	18 19 20 21 20 20 35 39	decmul2c	$$⊢2\cdot 420=840$$
41	40	oveq2i	$$⊢42\cdot 420=4\cdot 840$$
42	17 41	eqtri	$$⊢420\cdot 8=4\cdot 840$$
43	4 5 6 9 10 11 42	lcmeprodgcdi	$$⊢420\mathrm{lcm}8=840$$