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 ‘ 𝑍 ) ∈ ℕ )