Theorem lcm3un

Description: Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Assertion	lcm3un	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3\right)\right)=6$$

Proof

Step	Hyp	Ref	Expression
1		3nn	$$⊢3\in \mathbb{N}$$
2		id	$$⊢3\in \mathbb{N}\to 3\in \mathbb{N}$$
3	2	lcmfunnnd	$$⊢3\in \mathbb{N}\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3-1\right)\right)\mathrm{lcm}3$$
4	1 3	ax-mp	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3-1\right)\right)\mathrm{lcm}3$$
5		3m1e2	$$⊢3-1=2$$
6	5	oveq2i	$$⊢\left(1\dots 3-1\right)=\left(1\dots 2\right)$$
7	6	fveq2i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3-1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\right)\right)$$
8		lcm2un	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\right)\right)=2$$
9	7 8	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3-1\right)\right)=2$$
10	9	oveq1i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3-1\right)\right)\mathrm{lcm}3=2\mathrm{lcm}3$$
11		2z	$$⊢2\in \mathbb{Z}$$
12		3z	$$⊢3\in \mathbb{Z}$$
13	11 12	pm3.2i	$$⊢\left(2\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)$$
14		lcmcom	$$⊢\left(2\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to 2\mathrm{lcm}3=3\mathrm{lcm}2$$
15	13 14	ax-mp	$$⊢2\mathrm{lcm}3=3\mathrm{lcm}2$$
16		3lcm2e6	$$⊢3\mathrm{lcm}2=6$$
17	15 16	eqtri	$$⊢2\mathrm{lcm}3=6$$
18	10 17	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3-1\right)\right)\mathrm{lcm}3=6$$
19	4 18	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3\right)\right)=6$$