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

Metamath Proof Explorer

Theorem lcmfn0cl

Description: Closure of the _lcm function. (Contributed by AV, 21-Aug-2020)

Ref Expression
Assertion lcmfn0cl ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ ℕ

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ n ∈ ℕ | ∀ m ∈ Z m ∥ n ⊆ ℕ
2 lcmfcllem ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ n ∈ ℕ | ∀ m ∈ Z m ∥ n
3 1 2 sselid ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ ℕ