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

Metamath Proof Explorer

Theorem lcmfnncl

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

Ref Expression
Assertion lcmfnncl ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑍 ⊆ ℕ → 𝑍 ⊆ ℕ )
2 nnssz ⊢ ℕ ⊆ ℤ
3 1 2 sstrdi ⊢ ( 𝑍 ⊆ ℕ → 𝑍 ⊆ ℤ )
4 3 adantr ⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 𝑍 ⊆ ℤ )
5 simpr ⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 𝑍 ∈ Fin )
6 0nnn ⊢ ¬ 0 ∈ ℕ
7 ssel ⊢ ( 𝑍 ⊆ ℕ → ( 0 ∈ 𝑍 → 0 ∈ ℕ ) )
8 6 7 mtoi ⊢ ( 𝑍 ⊆ ℕ → ¬ 0 ∈ 𝑍 )
9 df-nel ⊢ ( 0 ∉ 𝑍 ↔ ¬ 0 ∈ 𝑍 )
10 8 9 sylibr ⊢ ( 𝑍 ⊆ ℕ → 0 ∉ 𝑍 )
11 10 adantr ⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 0 ∉ 𝑍 )
12 lcmfn0cl ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm ‘ 𝑍 ) ∈ ℕ )
13 4 5 11 12 syl3anc ⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) ∈ ℕ )