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 \mathbb{N}$$
2		9nn	$$⊢9\in \mathbb{N}$$
3	1 2	nnmulcli	$$⊢6\cdot 9\in \mathbb{N}$$
4	3	nncni	$$⊢6\cdot 9\in ℂ$$
5	1	nnzi	$$⊢6\in \mathbb{Z}$$
6	2	nnzi	$$⊢9\in \mathbb{Z}$$
7	5 6	pm3.2i	$$⊢\left(6\in \mathbb{Z}\wedge 9\in \mathbb{Z}\right)$$
8		lcmcl	$$⊢\left(6\in \mathbb{Z}\wedge 9\in \mathbb{Z}\right)\to 6\mathrm{lcm}9\in {\mathbb{N}}_0$$
9	8	nn0cnd	$$⊢\left(6\in \mathbb{Z}\wedge 9\in \mathbb{Z}\right)\to 6\mathrm{lcm}9\in ℂ$$
10	7 9	ax-mp	$$⊢6\mathrm{lcm}9\in ℂ$$
11		neggcd	$$⊢\left(6\in \mathbb{Z}\wedge 9\in \mathbb{Z}\right)\to -6\gcd 9=6\gcd 9$$
12	7 11	ax-mp	$$⊢-6\gcd 9=6\gcd 9$$
13	12	eqcomi	$$⊢6\gcd 9=-6\gcd 9$$
14		ex-gcd	$$⊢-6\gcd 9=3$$
15	13 14	eqtri	$$⊢6\gcd 9=3$$
16		3cn	$$⊢3\in ℂ$$
17	15 16	eqeltri	$$⊢6\gcd 9\in ℂ$$
18		3ne0	$$⊢3\ne 0$$
19	15 18	eqnetri	$$⊢6\gcd 9\ne 0$$
20	17 19	pm3.2i	$$⊢\left(6\gcd 9\in ℂ\wedge 6\gcd 9\ne 0\right)$$
21	1 2	pm3.2i	$$⊢\left(6\in \mathbb{N}\wedge 9\in \mathbb{N}\right)$$
22		lcmgcdnn	$$⊢\left(6\in \mathbb{N}\wedge 9\in \mathbb{N}\right)\to \left(6\mathrm{lcm}9\right)\left(6\gcd 9\right)=6\cdot 9$$
23	21 22	mp1i	$$⊢\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\gcd 9\in ℂ\wedge 6\gcd 9\ne 0\right)\right)\to \left(6\mathrm{lcm}9\right)\left(6\gcd 9\right)=6\cdot 9$$
24	23	eqcomd	$$⊢\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\gcd 9\in ℂ\wedge 6\gcd 9\ne 0\right)\right)\to 6\cdot 9=\left(6\mathrm{lcm}9\right)\left(6\gcd 9\right)$$
25		divmul3	$$⊢\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\gcd 9\in ℂ\wedge 6\gcd 9\ne 0\right)\right)\to \left(\frac{6\cdot 9}{6\gcd 9}=6\mathrm{lcm}9\leftrightarrow 6\cdot 9=\left(6\mathrm{lcm}9\right)\left(6\gcd 9\right)\right)$$
26	24 25	mpbird	$$⊢\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\gcd 9\in ℂ\wedge 6\gcd 9\ne 0\right)\right)\to \frac{6\cdot 9}{6\gcd 9}=6\mathrm{lcm}9$$
27	26	eqcomd	$$⊢\left(6\cdot 9\in ℂ\wedge 6\mathrm{lcm}9\in ℂ\wedge \left(6\gcd 9\in ℂ\wedge 6\gcd 9\ne 0\right)\right)\to 6\mathrm{lcm}9=\frac{6\cdot 9}{6\gcd 9}$$
28	4 10 20 27	mp3an	$$⊢6\mathrm{lcm}9=\frac{6\cdot 9}{6\gcd 9}$$
29	15	oveq2i	$$⊢\frac{6\cdot 9}{6\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$$