Theorem lcmf0

Description: The least common multiple of the empty set is 1. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

	Ref	Expression
Assertion	lcmf0	⊢ ( lcm ‘ ∅ ) = 1

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ ℤ
2		0fi	⊢ ∅ ∈ Fin
3		noel	⊢ ¬ 0 ∈ ∅
4	3	nelir	⊢ 0 ∉ ∅
5		lcmfn0val	⊢ ( ( ∅ ⊆ ℤ ∧ ∅ ∈ Fin ∧ 0 ∉ ∅ ) → ( lcm ‘ ∅ ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛 } , ℝ , < ) )
6	1 2 4 5	mp3an	⊢ ( lcm ‘ ∅ ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛 } , ℝ , < )
7		ral0	⊢ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛
8	7	rgenw	⊢ ∀ 𝑛 ∈ ℕ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛
9		rabid2	⊢ ( ℕ = { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛 } ↔ ∀ 𝑛 ∈ ℕ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛 )
10	8 9	mpbir	⊢ ℕ = { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛 }
11	10	eqcomi	⊢ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛 } = ℕ
12	11	infeq1i	⊢ inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛 } , ℝ , < ) = inf ( ℕ , ℝ , < )
13		nninf	⊢ inf ( ℕ , ℝ , < ) = 1
14	6 12 13	3eqtri	⊢ ( lcm ‘ ∅ ) = 1