Theorem lcmfnnval

Description: The value of the _lcm function for a subset of the positive integers. (Contributed by AV, 21-Aug-2020) (Revised by AV, 16-Sep-2020)

	Ref	Expression
Assertion	lcmfnnval	$$⊢\left(Z\subseteq \mathbb{N}\wedge Z\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=inf\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)$$

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	6	nelir	$$⊢0\notin \mathbb{N}$$
8		ssel	$$⊢Z\subseteq \mathbb{N}\to \left(0\in Z\to 0\in \mathbb{N}\right)$$
9	8	nelcon3d	$$⊢Z\subseteq \mathbb{N}\to \left(0\notin \mathbb{N}\to 0\notin Z\right)$$
10	7 9	mpi	$$⊢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		lcmfn0val	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\wedge 0\notin Z\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=inf\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)$$
13	4 5 11 12	syl3anc	$$⊢\left(Z\subseteq \mathbb{N}\wedge Z\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=inf\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)$$