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		4cn	$$⊢4\in ℂ$$
24		2cn	$$⊢2\in ℂ$$
25	23 24 13	mulcomli	$$⊢2\cdot 4=8$$
26	25	oveq1i	$$⊢2\cdot 4+0=8+0$$
27		8cn	$$⊢8\in ℂ$$
28	27	addridi	$$⊢8+0=8$$
29	26 28	eqtri	$$⊢2\cdot 4+0=8$$
30		2t2e4	$$⊢2\cdot 2=4$$
31	1	dec0h	$$⊢4=04$$
32	31	eqcomi	$$⊢04=4$$
33	30 32	eqtr4i	$$⊢2\cdot 2=04$$
34	18 1 18 22 1 20 29 33	decmul2c	$$⊢2\cdot 42=84$$
35	23	addridi	$$⊢4+0=4$$
36	7 1 20 34 35	decaddi	$$⊢2\cdot 42+0=84$$
37		2t0e0	$$⊢2\cdot 0=0$$
38	20	dec0h	$$⊢0=00$$
39	38	eqcomi	$$⊢00=0$$
40	37 39	eqtr4i	$$⊢2\cdot 0=00$$
41	18 19 20 21 20 20 36 40	decmul2c	$$⊢2\cdot 420=840$$
42	41	oveq2i	$$⊢42\cdot 420=4\cdot 840$$
43	17 42	eqtri	$$⊢420\cdot 8=4\cdot 840$$
44	4 5 6 9 10 11 43	lcmeprodgcdi	$$⊢420\mathrm{lcm}8=840$$