Theorem lcmfnncl

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

	Ref	Expression
Assertion	lcmfnncl	$$⊢\left(Z\subseteq \mathbb{N}\wedge Z\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)\in \mathbb{N}$$

Proof

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