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 {\mathbb{N}}_0$$
5	4	nn0zi	$$⊢6\in \mathbb{Z}$$
6		4z	$$⊢4\in \mathbb{Z}$$
7		lcmcl	$$⊢\left(6\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to 6\mathrm{lcm}4\in {\mathbb{N}}_0$$
8	7	nn0cnd	$$⊢\left(6\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to 6\mathrm{lcm}4\in ℂ$$
9	5 6 8	mp2an	$$⊢6\mathrm{lcm}4\in ℂ$$
10		gcdcl	$$⊢\left(6\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to 6\gcd 4\in {\mathbb{N}}_0$$
11	10	nn0cnd	$$⊢\left(6\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to 6\gcd 4\in ℂ$$
12	5 6 11	mp2an	$$⊢6\gcd 4\in ℂ$$
13	5 6	pm3.2i	$$⊢\left(6\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)$$
14		4ne0	$$⊢4\ne 0$$
15	14	neii	$$⊢\neg 4=0$$
16	15	intnan	$$⊢\neg \left(6=0\wedge 4=0\right)$$
17		gcdn0cl	$$⊢\left(\left(6\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\wedge \neg \left(6=0\wedge 4=0\right)\right)\to 6\gcd 4\in \mathbb{N}$$
18	13 16 17	mp2an	$$⊢6\gcd 4\in \mathbb{N}$$
19	18	nnne0i	$$⊢6\gcd 4\ne 0$$
20	12 19	pm3.2i	$$⊢\left(6\gcd 4\in ℂ\wedge 6\gcd 4\ne 0\right)$$
21		6nn	$$⊢6\in \mathbb{N}$$
22		4nn	$$⊢4\in \mathbb{N}$$
23	21 22	pm3.2i	$$⊢\left(6\in \mathbb{N}\wedge 4\in \mathbb{N}\right)$$
24		lcmgcdnn	$$⊢\left(6\in \mathbb{N}\wedge 4\in \mathbb{N}\right)\to \left(6\mathrm{lcm}4\right)\left(6\gcd 4\right)=6\cdot 4$$
25	23 24	mp1i	$$⊢\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\gcd 4\in ℂ\wedge 6\gcd 4\ne 0\right)\right)\to \left(6\mathrm{lcm}4\right)\left(6\gcd 4\right)=6\cdot 4$$
26	25	eqcomd	$$⊢\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\gcd 4\in ℂ\wedge 6\gcd 4\ne 0\right)\right)\to 6\cdot 4=\left(6\mathrm{lcm}4\right)\left(6\gcd 4\right)$$
27		divmul3	$$⊢\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\gcd 4\in ℂ\wedge 6\gcd 4\ne 0\right)\right)\to \left(\frac{6\cdot 4}{6\gcd 4}=6\mathrm{lcm}4\leftrightarrow 6\cdot 4=\left(6\mathrm{lcm}4\right)\left(6\gcd 4\right)\right)$$
28	26 27	mpbird	$$⊢\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\gcd 4\in ℂ\wedge 6\gcd 4\ne 0\right)\right)\to \frac{6\cdot 4}{6\gcd 4}=6\mathrm{lcm}4$$
29	28	eqcomd	$$⊢\left(6\cdot 4\in ℂ\wedge 6\mathrm{lcm}4\in ℂ\wedge \left(6\gcd 4\in ℂ\wedge 6\gcd 4\ne 0\right)\right)\to 6\mathrm{lcm}4=\frac{6\cdot 4}{6\gcd 4}$$
30	3 9 20 29	mp3an	$$⊢6\mathrm{lcm}4=\frac{6\cdot 4}{6\gcd 4}$$
31		6gcd4e2	$$⊢6\gcd 4=2$$
32	31	oveq2i	$$⊢\frac{6\cdot 4}{6\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$$