Theorem lcm1un

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

	Ref	Expression
Assertion	lcm1un	⊢ ( lcm ‘ ( 1 ... 1 ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		id	⊢ ( 1 ∈ ℕ → 1 ∈ ℕ )
3	2	lcmfunnnd	⊢ ( 1 ∈ ℕ → ( lcm ‘ ( 1 ... 1 ) ) = ( ( lcm ‘ ( 1 ... ( 1 − 1 ) ) ) lcm 1 ) )
4	1 3	ax-mp	⊢ ( lcm ‘ ( 1 ... 1 ) ) = ( ( lcm ‘ ( 1 ... ( 1 − 1 ) ) ) lcm 1 )
5		1m1e0	⊢ ( 1 − 1 ) = 0
6	5	oveq2i	⊢ ( 1 ... ( 1 − 1 ) ) = ( 1 ... 0 )
7		fz10	⊢ ( 1 ... 0 ) = ∅
8	6 7	eqtri	⊢ ( 1 ... ( 1 − 1 ) ) = ∅
9	8	fveq2i	⊢ ( lcm ‘ ( 1 ... ( 1 − 1 ) ) ) = ( lcm ‘ ∅ )
10		lcmf0	⊢ ( lcm ‘ ∅ ) = 1
11	9 10	eqtri	⊢ ( lcm ‘ ( 1 ... ( 1 − 1 ) ) ) = 1
12	11	oveq1i	⊢ ( ( lcm ‘ ( 1 ... ( 1 − 1 ) ) ) lcm 1 ) = ( 1 lcm 1 )
13		1z	⊢ 1 ∈ ℤ
14		lcmid	⊢ ( 1 ∈ ℤ → ( 1 lcm 1 ) = ( abs ‘ 1 ) )
15	13 14	ax-mp	⊢ ( 1 lcm 1 ) = ( abs ‘ 1 )
16		abs1	⊢ ( abs ‘ 1 ) = 1
17	15 16	eqtri	⊢ ( 1 lcm 1 ) = 1
18	12 17	eqtri	⊢ ( ( lcm ‘ ( 1 ... ( 1 − 1 ) ) ) lcm 1 ) = 1
19	4 18	eqtri	⊢ ( lcm ‘ ( 1 ... 1 ) ) = 1