Theorem fissn0dvdsn0

Description: For each finite subset of the integers not containing 0 there is a positive integer which is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020)

	Ref	Expression
Assertion	fissn0dvdsn0	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\wedge 0\notin Z\right)\to \left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fissn0dvds	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\wedge 0\notin Z\right)\to \exists n\in \mathbb{N}\forall m\in Zm\parallel n$$
2		rabn0	$$⊢\left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\}\ne \varnothing \leftrightarrow \exists n\in \mathbb{N}\forall m\in Zm\parallel n$$
3	1 2	sylibr	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\wedge 0\notin Z\right)\to \left\{n\in \mathbb{N}|\forall m\in Zm\parallel n\right\}\ne \varnothing$$