Theorem lcmfn0val

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

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

Proof

Step	Hyp	Ref	Expression
1		lcmfval	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=if\left(0\in Z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)\right)$$
2	1	3adant3	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\wedge 0\notin Z\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=if\left(0\in Z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)\right)$$
3		df-nel	$$⊢0\notin Z\leftrightarrow \neg 0\in Z$$
4		iffalse	$$⊢\neg 0\in Z\to if\left(0\in Z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)\right)=sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)$$
5	3 4	sylbi	$$⊢0\notin Z\to if\left(0\in Z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)\right)=sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)$$
6	5	3ad2ant3	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\wedge 0\notin Z\right)\to if\left(0\in Z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)\right)=sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)$$
7	2 6	eqtrd	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\wedge 0\notin Z\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=sup\left(\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\},ℝ,<\right)$$