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 |
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 |