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 0fin ⊢∅∈Fin
3 noel ⊢¬0∈∅
4 3 nelir ⊢0∉∅
5 lcmfn0val ⊢∅⊆ℤ∧∅∈Fin∧0∉∅→lcm_⁡∅=supn∈ℕ|∀m∈∅m∥nℝ<
6 1 2 4 5 mp3an ⊢lcm_⁡∅=supn∈ℕ|∀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 ⊢supn∈ℕ|∀m∈∅m∥nℝ<=supℕℝ<
13 nninf ⊢supℕℝ<=1
14 6 12 13 3eqtri ⊢lcm_⁡∅=1