lcmfnncl

		Ref	Expression
	Assertion	lcmfnncl	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to \underline{lcm} (Z) \in ℕ$

Step	Hyp	Ref	Expression
1		id	$⊢ Z \subseteq ℕ \to Z \subseteq ℕ$
2		nnssz	$⊢ ℕ \subseteq ℤ$
3	1 2	sstrdi	$⊢ Z \subseteq ℕ \to Z \subseteq ℤ$
4	3	adantr	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to Z \subseteq ℤ$
5		simpr	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to Z \in Fin$
6		0nnn	$⊢ \neg 0 \in ℕ$
7		ssel	$⊢ Z \subseteq ℕ \to (0 \in Z \to 0 \in ℕ)$
8	6 7	mtoi	$⊢ Z \subseteq ℕ \to \neg 0 \in Z$
9		df-nel	$⊢ 0 \notin Z \leftrightarrow \neg 0 \in Z$
10	8 9	sylibr	$⊢ Z \subseteq ℕ \to 0 \notin Z$
11	10	adantr	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to 0 \notin Z$
12		lcmfn0cl	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \underline{lcm} (Z) \in ℕ$
13	4 5 11 12	syl3anc	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to \underline{lcm} (Z) \in ℕ$

Metamath Proof Explorer