Metamath Proof Explorer

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 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 = 0 4
32 31 eqcomi ⊢ 0 4 = 4
33 30 32 eqtr4i ⊢ ( 2 · 2 ) = 0 4
34 18 1 18 22 1 20 29 33 decmul2c ⊢ ( 2 · 4 2 ) = 8 4
35 23 addid1i ⊢ ( 4 + 0 ) = 4
36 7 1 20 34 35 decaddi ⊢ ( ( 2 · 4 2 ) + 0 ) = 8 4
37 2t0e0 ⊢ ( 2 · 0 ) = 0
38 20 dec0h ⊢ 0 = 0 0
39 38 eqcomi ⊢ 0 0 = 0
40 37 39 eqtr4i ⊢ ( 2 · 0 ) = 0 0
41 18 19 20 21 20 20 36 40 decmul2c ⊢ ( 2 · 4 2 0 ) = 8 4 0
42 41 oveq2i ⊢ ( 4 · ( 2 · 4 2 0 ) ) = ( 4 · 8 4 0 )
43 17 42 eqtri ⊢ ( 4 2 0 · 8 ) = ( 4 · 8 4 0 )
44 4 5 6 9 10 11 43 lcmeprodgcdi ⊢ ( 4 2 0 lcm 8 ) = 8 4 0