Theorem lcmfeq0b

Description: The least common multiple of a set of integers is 0 iff at least one of its element is 0. (Contributed by AV, 21-Aug-2020)

	Ref	Expression
Assertion	lcmfeq0b	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left(\underset{\_}{\mathrm{lcm}}\left(Z\right)=0\leftrightarrow 0\in Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$$⊢0\notin Z\leftrightarrow \neg 0\in Z$$
2		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}$$
3	2	nnne0d	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\wedge 0\notin Z\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)\ne 0$$
4	3	3expia	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left(0\notin Z\to \underset{\_}{\mathrm{lcm}}\left(Z\right)\ne 0\right)$$
5	1 4	biimtrrid	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left(\neg 0\in Z\to \underset{\_}{\mathrm{lcm}}\left(Z\right)\ne 0\right)$$
6	5	necon4bd	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left(\underset{\_}{\mathrm{lcm}}\left(Z\right)=0\to 0\in Z\right)$$
7		lcmf0val	$$⊢\left(Z\subseteq \mathbb{Z}\wedge 0\in Z\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=0$$
8	7	ex	$$⊢Z\subseteq \mathbb{Z}\to \left(0\in Z\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=0\right)$$
9	8	adantr	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left(0\in Z\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=0\right)$$
10	6 9	impbid	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left(\underset{\_}{\mathrm{lcm}}\left(Z\right)=0\leftrightarrow 0\in Z\right)$$