lcm2un

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

		Ref	Expression
	Assertion	lcm2un	$⊢ \underline{lcm} ((1 \dots 2)) = 2$

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

Metamath Proof Explorer