# Metamath Proof Explorer

## Theorem 6lcm4e12

Description: The least common multiple of six and four is twelve. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion 6lcm4e12 ${⊢}6\mathrm{lcm}4=12$

### Proof

Step Hyp Ref Expression
1 6cn ${⊢}6\in ℂ$
2 4cn ${⊢}4\in ℂ$
3 1 2 mulcli ${⊢}6\cdot 4\in ℂ$
4 6nn0 ${⊢}6\in {ℕ}_{0}$
5 4 nn0zi ${⊢}6\in ℤ$
6 4z ${⊢}4\in ℤ$
7 lcmcl ${⊢}\left(6\in ℤ\wedge 4\in ℤ\right)\to 6\mathrm{lcm}4\in {ℕ}_{0}$
8 7 nn0cnd ${⊢}\left(6\in ℤ\wedge 4\in ℤ\right)\to 6\mathrm{lcm}4\in ℂ$
9 5 6 8 mp2an ${⊢}6\mathrm{lcm}4\in ℂ$
10 gcdcl ${⊢}\left(6\in ℤ\wedge 4\in ℤ\right)\to 6\mathrm{gcd}4\in {ℕ}_{0}$
11 10 nn0cnd ${⊢}\left(6\in ℤ\wedge 4\in ℤ\right)\to 6\mathrm{gcd}4\in ℂ$
12 5 6 11 mp2an ${⊢}6\mathrm{gcd}4\in ℂ$
13 5 6 pm3.2i ${⊢}\left(6\in ℤ\wedge 4\in ℤ\right)$
14 4ne0 ${⊢}4\ne 0$
15 14 neii ${⊢}¬4=0$
16 15 intnan ${⊢}¬\left(6=0\wedge 4=0\right)$
17 gcdn0cl ${⊢}\left(\left(6\in ℤ\wedge 4\in ℤ\right)\wedge ¬\left(6=0\wedge 4=0\right)\right)\to 6\mathrm{gcd}4\in ℕ$
18 13 16 17 mp2an ${⊢}6\mathrm{gcd}4\in ℕ$
19 18 nnne0i ${⊢}6\mathrm{gcd}4\ne 0$
20 12 19 pm3.2i ${⊢}\left(6\mathrm{gcd}4\in ℂ\wedge 6\mathrm{gcd}4\ne 0\right)$
21 6nn ${⊢}6\in ℕ$
22 4nn ${⊢}4\in ℕ$
23 21 22 pm3.2i ${⊢}\left(6\in ℕ\wedge 4\in ℕ\right)$
24 lcmgcdnn ${⊢}\left(6\in ℕ\wedge 4\in ℕ\right)\to \left(6\mathrm{lcm}4\right)\left(6\mathrm{gcd}4\right)=6\cdot 4$
25 23 24 mp1i ${⊢}\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\mathrm{gcd}4\in ℂ\wedge 6\mathrm{gcd}4\ne 0\right)\right)\to \left(6\mathrm{lcm}4\right)\left(6\mathrm{gcd}4\right)=6\cdot 4$
26 25 eqcomd ${⊢}\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\mathrm{gcd}4\in ℂ\wedge 6\mathrm{gcd}4\ne 0\right)\right)\to 6\cdot 4=\left(6\mathrm{lcm}4\right)\left(6\mathrm{gcd}4\right)$
27 divmul3 ${⊢}\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\mathrm{gcd}4\in ℂ\wedge 6\mathrm{gcd}4\ne 0\right)\right)\to \left(\frac{6\cdot 4}{6\mathrm{gcd}4}=6\mathrm{lcm}4↔6\cdot 4=\left(6\mathrm{lcm}4\right)\left(6\mathrm{gcd}4\right)\right)$
28 26 27 mpbird ${⊢}\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\mathrm{gcd}4\in ℂ\wedge 6\mathrm{gcd}4\ne 0\right)\right)\to \frac{6\cdot 4}{6\mathrm{gcd}4}=6\mathrm{lcm}4$
29 28 eqcomd ${⊢}\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\mathrm{gcd}4\in ℂ\wedge 6\mathrm{gcd}4\ne 0\right)\right)\to 6\mathrm{lcm}4=\frac{6\cdot 4}{6\mathrm{gcd}4}$
30 3 9 20 29 mp3an ${⊢}6\mathrm{lcm}4=\frac{6\cdot 4}{6\mathrm{gcd}4}$
31 6gcd4e2 ${⊢}6\mathrm{gcd}4=2$
32 31 oveq2i ${⊢}\frac{6\cdot 4}{6\mathrm{gcd}4}=\frac{6\cdot 4}{2}$
33 2cn ${⊢}2\in ℂ$
34 2ne0 ${⊢}2\ne 0$
35 1 2 33 34 divassi ${⊢}\frac{6\cdot 4}{2}=6\left(\frac{4}{2}\right)$
36 4d2e2 ${⊢}\frac{4}{2}=2$
37 36 oveq2i ${⊢}6\left(\frac{4}{2}\right)=6\cdot 2$
38 6t2e12 ${⊢}6\cdot 2=12$
39 35 37 38 3eqtri ${⊢}\frac{6\cdot 4}{2}=12$
40 30 32 39 3eqtri ${⊢}6\mathrm{lcm}4=12$