This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑛 } , ℝ , < ) )
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