Theorem lcm2un

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

	Ref	Expression
Assertion	lcm2un	⊢ ( lcm ‘ ( 1 ... 2 ) ) = 2

Proof

Step	Hyp	Ref	Expression
1		2nn	⊢ 2 ∈ ℕ
2		id	⊢ ( 2 ∈ ℕ → 2 ∈ ℕ )
3	2	lcmfunnnd	⊢ ( 2 ∈ ℕ → ( lcm ‘ ( 1 ... 2 ) ) = ( ( lcm ‘ ( 1 ... ( 2 − 1 ) ) ) lcm 2 ) )
4	1 3	ax-mp	⊢ ( lcm ‘ ( 1 ... 2 ) ) = ( ( lcm ‘ ( 1 ... ( 2 − 1 ) ) ) lcm 2 )
5		2m1e1	⊢ ( 2 − 1 ) = 1
6	5	oveq2i	⊢ ( 1 ... ( 2 − 1 ) ) = ( 1 ... 1 )
7	6	fveq2i	⊢ ( lcm ‘ ( 1 ... ( 2 − 1 ) ) ) = ( lcm ‘ ( 1 ... 1 ) )
8	7	oveq1i	⊢ ( ( lcm ‘ ( 1 ... ( 2 − 1 ) ) ) lcm 2 ) = ( ( lcm ‘ ( 1 ... 1 ) ) lcm 2 )
9	4 8	eqtri	⊢ ( lcm ‘ ( 1 ... 2 ) ) = ( ( lcm ‘ ( 1 ... 1 ) ) lcm 2 )
10		lcm1un	⊢ ( lcm ‘ ( 1 ... 1 ) ) = 1
11	10	oveq1i	⊢ ( ( lcm ‘ ( 1 ... 1 ) ) lcm 2 ) = ( 1 lcm 2 )
12		1z	⊢ 1 ∈ ℤ
13		2z	⊢ 2 ∈ ℤ
14		lcmcom	⊢ ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 1 lcm 2 ) = ( 2 lcm 1 ) )
15	12 13 14	mp2an	⊢ ( 1 lcm 2 ) = ( 2 lcm 1 )
16		lcm1	⊢ ( 2 ∈ ℤ → ( 2 lcm 1 ) = ( abs ‘ 2 ) )
17	13 16	ax-mp	⊢ ( 2 lcm 1 ) = ( abs ‘ 2 )
18		2re	⊢ 2 ∈ ℝ
19		0le2	⊢ 0 ≤ 2
20	18 19	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 ≤ 2 )
21		absid	⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( abs ‘ 2 ) = 2 )
22	20 21	ax-mp	⊢ ( abs ‘ 2 ) = 2
23	17 22	eqtri	⊢ ( 2 lcm 1 ) = 2
24	15 23	eqtri	⊢ ( 1 lcm 2 ) = 2
25	11 24	eqtri	⊢ ( ( lcm ‘ ( 1 ... 1 ) ) lcm 2 ) = 2
26	9 25	eqtri	⊢ ( lcm ‘ ( 1 ... 2 ) ) = 2