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

Metamath Proof Explorer

Theorem lcmfcl

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

Ref Expression
Assertion lcmfcl ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) ∈ ℕ0 )

Proof

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