Metamath Proof Explorer


Theorem 420lcm8e840

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

Ref Expression
Assertion 420lcm8e840 420 lcm 8 = 840

Proof

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