# Metamath Proof Explorer

## Theorem ex-lcm

Description: Example for df-lcm . (Contributed by AV, 5-Sep-2021)

Ref Expression
Assertion ex-lcm ${⊢}6\mathrm{lcm}9=18$

### Proof

Step Hyp Ref Expression
1 6nn ${⊢}6\in ℕ$
2 9nn ${⊢}9\in ℕ$
3 1 2 nnmulcli ${⊢}6\cdot 9\in ℕ$
4 3 nncni ${⊢}6\cdot 9\in ℂ$
5 1 nnzi ${⊢}6\in ℤ$
6 2 nnzi ${⊢}9\in ℤ$
7 5 6 pm3.2i ${⊢}\left(6\in ℤ\wedge 9\in ℤ\right)$
8 lcmcl ${⊢}\left(6\in ℤ\wedge 9\in ℤ\right)\to 6\mathrm{lcm}9\in {ℕ}_{0}$
9 8 nn0cnd ${⊢}\left(6\in ℤ\wedge 9\in ℤ\right)\to 6\mathrm{lcm}9\in ℂ$
10 7 9 ax-mp ${⊢}6\mathrm{lcm}9\in ℂ$
11 neggcd ${⊢}\left(6\in ℤ\wedge 9\in ℤ\right)\to -6\mathrm{gcd}9=6\mathrm{gcd}9$
12 7 11 ax-mp ${⊢}-6\mathrm{gcd}9=6\mathrm{gcd}9$
13 12 eqcomi ${⊢}6\mathrm{gcd}9=-6\mathrm{gcd}9$
14 ex-gcd ${⊢}-6\mathrm{gcd}9=3$
15 13 14 eqtri ${⊢}6\mathrm{gcd}9=3$
16 3cn ${⊢}3\in ℂ$
17 15 16 eqeltri ${⊢}6\mathrm{gcd}9\in ℂ$
18 3ne0 ${⊢}3\ne 0$
19 15 18 eqnetri ${⊢}6\mathrm{gcd}9\ne 0$
20 17 19 pm3.2i ${⊢}\left(6\mathrm{gcd}9\in ℂ\wedge 6\mathrm{gcd}9\ne 0\right)$
21 1 2 pm3.2i ${⊢}\left(6\in ℕ\wedge 9\in ℕ\right)$
22 lcmgcdnn ${⊢}\left(6\in ℕ\wedge 9\in ℕ\right)\to \left(6\mathrm{lcm}9\right)\left(6\mathrm{gcd}9\right)=6\cdot 9$
23 21 22 mp1i ${⊢}\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\mathrm{gcd}9\in ℂ\wedge 6\mathrm{gcd}9\ne 0\right)\right)\to \left(6\mathrm{lcm}9\right)\left(6\mathrm{gcd}9\right)=6\cdot 9$
24 23 eqcomd ${⊢}\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\mathrm{gcd}9\in ℂ\wedge 6\mathrm{gcd}9\ne 0\right)\right)\to 6\cdot 9=\left(6\mathrm{lcm}9\right)\left(6\mathrm{gcd}9\right)$
25 divmul3 ${⊢}\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\mathrm{gcd}9\in ℂ\wedge 6\mathrm{gcd}9\ne 0\right)\right)\to \left(\frac{6\cdot 9}{6\mathrm{gcd}9}=6\mathrm{lcm}9↔6\cdot 9=\left(6\mathrm{lcm}9\right)\left(6\mathrm{gcd}9\right)\right)$
26 24 25 mpbird ${⊢}\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\mathrm{gcd}9\in ℂ\wedge 6\mathrm{gcd}9\ne 0\right)\right)\to \frac{6\cdot 9}{6\mathrm{gcd}9}=6\mathrm{lcm}9$
27 26 eqcomd ${⊢}\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\mathrm{gcd}9\in ℂ\wedge 6\mathrm{gcd}9\ne 0\right)\right)\to 6\mathrm{lcm}9=\frac{6\cdot 9}{6\mathrm{gcd}9}$
28 4 10 20 27 mp3an ${⊢}6\mathrm{lcm}9=\frac{6\cdot 9}{6\mathrm{gcd}9}$
29 15 oveq2i ${⊢}\frac{6\cdot 9}{6\mathrm{gcd}9}=\frac{6\cdot 9}{3}$
30 6cn ${⊢}6\in ℂ$
31 9cn ${⊢}9\in ℂ$
32 30 31 16 18 divassi ${⊢}\frac{6\cdot 9}{3}=6\left(\frac{9}{3}\right)$
33 3t3e9 ${⊢}3\cdot 3=9$
34 33 eqcomi ${⊢}9=3\cdot 3$
35 34 oveq1i ${⊢}\frac{9}{3}=\frac{3\cdot 3}{3}$
36 16 16 18 divcan3i ${⊢}\frac{3\cdot 3}{3}=3$
37 35 36 eqtri ${⊢}\frac{9}{3}=3$
38 37 oveq2i ${⊢}6\left(\frac{9}{3}\right)=6\cdot 3$
39 6t3e18 ${⊢}6\cdot 3=18$
40 32 38 39 3eqtri ${⊢}\frac{6\cdot 9}{3}=18$
41 28 29 40 3eqtri ${⊢}6\mathrm{lcm}9=18$