Metamath Proof Explorer

Theorem lcmfcl

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

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

Proof

Step Hyp Ref Expression
1 lcmf0val ⊢ Z ⊆ ℤ ∧ 0 ∈ Z → lcm _ ⁡ Z = 0
2 0nn0 ⊢ 0 ∈ ℕ 0
3 1 2 eqeltrdi ⊢ Z ⊆ ℤ ∧ 0 ∈ Z → lcm _ ⁡ Z ∈ ℕ 0
4 3 adantlr ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∈ Z → lcm _ ⁡ Z ∈ ℕ 0
5 df-nel ⊢ 0 ∉ Z ↔ ¬ 0 ∈ Z
6 lcmfn0cl ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ ℕ
7 6 3expa ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ ℕ
8 5 7 sylan2br ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ ¬ 0 ∈ Z → lcm _ ⁡ Z ∈ ℕ
9 8 nnnn0d ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ ¬ 0 ∈ Z → lcm _ ⁡ Z ∈ ℕ 0
10 4 9 pm2.61dan ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → lcm _ ⁡ Z ∈ ℕ 0