Theorem lcm2un

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

	Ref	Expression
Assertion	lcm2un	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\right)\right)=2$$

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		id	$$⊢2\in \mathbb{N}\to 2\in \mathbb{N}$$
3	2	lcmfunnnd	$$⊢2\in \mathbb{N}\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2-1\right)\right)\mathrm{lcm}2$$
4	1 3	ax-mp	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2-1\right)\right)\mathrm{lcm}2$$
5		2m1e1	$$⊢2-1=1$$
6	5	oveq2i	$$⊢\left(1\dots 2-1\right)=\left(1\dots 1\right)$$
7	6	fveq2i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2-1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)$$
8	7	oveq1i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2-1\right)\right)\mathrm{lcm}2=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)\mathrm{lcm}2$$
9	4 8	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)\mathrm{lcm}2$$
10		lcm1un	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)=1$$
11	10	oveq1i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)\mathrm{lcm}2=1\mathrm{lcm}2$$
12		1z	$$⊢1\in \mathbb{Z}$$
13		2z	$$⊢2\in \mathbb{Z}$$
14		lcmcom	$$⊢\left(1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 1\mathrm{lcm}2=2\mathrm{lcm}1$$
15	12 13 14	mp2an	$$⊢1\mathrm{lcm}2=2\mathrm{lcm}1$$
16		lcm1	$$⊢2\in \mathbb{Z}\to 2\mathrm{lcm}1=\left|2\right|$$
17	13 16	ax-mp	$$⊢2\mathrm{lcm}1=\left|2\right|$$
18		2re	$$⊢2\in ℝ$$
19		0le2	$$⊢0\le 2$$
20	18 19	pm3.2i	$$⊢\left(2\in ℝ\wedge 0\le 2\right)$$
21		absid	$$⊢\left(2\in ℝ\wedge 0\le 2\right)\to \left|2\right|=2$$
22	20 21	ax-mp	$$⊢\left|2\right|=2$$
23	17 22	eqtri	$$⊢2\mathrm{lcm}1=2$$
24	15 23	eqtri	$$⊢1\mathrm{lcm}2=2$$
25	11 24	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)\mathrm{lcm}2=2$$
26	9 25	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\right)\right)=2$$