Theorem lcm3un

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

	Ref	Expression
Assertion	lcm3un	⊢ ( lcm ‘ ( 1 ... 3 ) ) = 6

Proof

Step	Hyp	Ref	Expression
1		3nn	⊢ 3 ∈ ℕ
2		id	⊢ ( 3 ∈ ℕ → 3 ∈ ℕ )
3	2	lcmfunnnd	⊢ ( 3 ∈ ℕ → ( lcm ‘ ( 1 ... 3 ) ) = ( ( lcm ‘ ( 1 ... ( 3 − 1 ) ) ) lcm 3 ) )
4	1 3	ax-mp	⊢ ( lcm ‘ ( 1 ... 3 ) ) = ( ( lcm ‘ ( 1 ... ( 3 − 1 ) ) ) lcm 3 )
5		3m1e2	⊢ ( 3 − 1 ) = 2
6	5	oveq2i	⊢ ( 1 ... ( 3 − 1 ) ) = ( 1 ... 2 )
7	6	fveq2i	⊢ ( lcm ‘ ( 1 ... ( 3 − 1 ) ) ) = ( lcm ‘ ( 1 ... 2 ) )
8		lcm2un	⊢ ( lcm ‘ ( 1 ... 2 ) ) = 2
9	7 8	eqtri	⊢ ( lcm ‘ ( 1 ... ( 3 − 1 ) ) ) = 2
10	9	oveq1i	⊢ ( ( lcm ‘ ( 1 ... ( 3 − 1 ) ) ) lcm 3 ) = ( 2 lcm 3 )
11		2z	⊢ 2 ∈ ℤ
12		3z	⊢ 3 ∈ ℤ
13	11 12	pm3.2i	⊢ ( 2 ∈ ℤ ∧ 3 ∈ ℤ )
14		lcmcom	⊢ ( ( 2 ∈ ℤ ∧ 3 ∈ ℤ ) → ( 2 lcm 3 ) = ( 3 lcm 2 ) )
15	13 14	ax-mp	⊢ ( 2 lcm 3 ) = ( 3 lcm 2 )
16		3lcm2e6	⊢ ( 3 lcm 2 ) = 6
17	15 16	eqtri	⊢ ( 2 lcm 3 ) = 6
18	10 17	eqtri	⊢ ( ( lcm ‘ ( 1 ... ( 3 − 1 ) ) ) lcm 3 ) = 6
19	4 18	eqtri	⊢ ( lcm ‘ ( 1 ... 3 ) ) = 6