lcmfcl

		Ref	Expression
	Assertion	lcmfcl	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to \underline{lcm} (Z) \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		lcmf0val	$⊢ (Z \subseteq ℤ \land 0 \in Z) \to \underline{lcm} (Z) = 0$
2		0nn0	$⊢ 0 \in ℕ_{0}$
3	1 2	eqeltrdi	$⊢ (Z \subseteq ℤ \land 0 \in Z) \to \underline{lcm} (Z) \in ℕ_{0}$
4	3	adantlr	$⊢ ((Z \subseteq ℤ \land Z \in Fin) \land 0 \in Z) \to \underline{lcm} (Z) \in ℕ_{0}$
5		df-nel	$⊢ 0 \notin Z \leftrightarrow \neg 0 \in Z$
6		lcmfn0cl	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \underline{lcm} (Z) \in ℕ$
7	6	3expa	$⊢ ((Z \subseteq ℤ \land Z \in Fin) \land 0 \notin Z) \to \underline{lcm} (Z) \in ℕ$
8	5 7	sylan2br	$⊢ ((Z \subseteq ℤ \land Z \in Fin) \land \neg 0 \in Z) \to \underline{lcm} (Z) \in ℕ$
9	8	nnnn0d	$⊢ ((Z \subseteq ℤ \land Z \in Fin) \land \neg 0 \in Z) \to \underline{lcm} (Z) \in ℕ_{0}$
10	4 9	pm2.61dan	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to \underline{lcm} (Z) \in ℕ_{0}$

Metamath Proof Explorer