Metamath Proof Explorer

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 n ∈ ℕ | ∀ m ∈ ∅ m ∥ n ℝ <
6 1 2 4 5 mp3an ⊢ lcm _ ⁡ ∅ = inf n ∈ ℕ | ∀ m ∈ ∅ m ∥ n ℝ <
7 ral0 ⊢ ∀ m ∈ ∅ m ∥ n
8 7 rgenw ⊢ ∀ n ∈ ℕ ∀ m ∈ ∅ m ∥ n
9 rabid2 ⊢ ℕ = n ∈ ℕ | ∀ m ∈ ∅ m ∥ n ↔ ∀ n ∈ ℕ ∀ m ∈ ∅ m ∥ n
10 8 9 mpbir ⊢ ℕ = n ∈ ℕ | ∀ m ∈ ∅ m ∥ n
11 10 eqcomi ⊢ n ∈ ℕ | ∀ m ∈ ∅ m ∥ n = ℕ
12 11 infeq1i ⊢ inf n ∈ ℕ | ∀ m ∈ ∅ m ∥ n ℝ < = inf ℕ ℝ <
13 nninf ⊢ inf ℕ ℝ < = 1
14 6 12 13 3eqtri ⊢ lcm _ ⁡ ∅ = 1