Metamath Proof Explorer


Theorem 60lcm7e420

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

Ref Expression
Assertion 60lcm7e420 ( 6 0 lcm 7 ) = 4 2 0

Proof

Step Hyp Ref Expression
1 6nn 6 ∈ ℕ
2 1 decnncl2 6 0 ∈ ℕ
3 7nn 7 ∈ ℕ
4 1nn 1 ∈ ℕ
5 4nn0 4 ∈ ℕ0
6 2nn 2 ∈ ℕ
7 5 6 decnncl 4 2 ∈ ℕ
8 7 decnncl2 4 2 0 ∈ ℕ
9 60gcd7e1 ( 6 0 gcd 7 ) = 1
10 2nn0 2 ∈ ℕ0
11 5 10 deccl 4 2 ∈ ℕ0
12 0nn0 0 ∈ ℕ0
13 11 12 deccl 4 2 0 ∈ ℕ0
14 13 nn0cni 4 2 0 ∈ ℂ
15 14 mulid2i ( 1 · 4 2 0 ) = 4 2 0
16 7nn0 7 ∈ ℕ0
17 6nn0 6 ∈ ℕ0
18 eqid 6 0 = 6 0
19 7cn 7 ∈ ℂ
20 6cn 6 ∈ ℂ
21 7t6e42 ( 7 · 6 ) = 4 2
22 19 20 21 mulcomli ( 6 · 7 ) = 4 2
23 2cn 2 ∈ ℂ
24 23 addid1i ( 2 + 0 ) = 2
25 5 10 12 22 24 decaddi ( ( 6 · 7 ) + 0 ) = 4 2
26 0cn 0 ∈ ℂ
27 19 mul01i ( 7 · 0 ) = 0
28 12 dec0h 0 = 0 0
29 28 eqcomi 0 0 = 0
30 27 29 eqtr4i ( 7 · 0 ) = 0 0
31 19 26 30 mulcomli ( 0 · 7 ) = 0 0
32 16 17 12 18 12 12 25 31 decmul1c ( 6 0 · 7 ) = 4 2 0
33 2 3 4 8 9 15 32 lcmeprodgcdi ( 6 0 lcm 7 ) = 4 2 0