Theorem uzn0bi

Description: The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	uzn0bi	$$⊢{\mathbb{Z}}_{\ge M}\ne \varnothing \leftrightarrow M\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		uz0	$$⊢\neg M\in \mathbb{Z}\to {\mathbb{Z}}_{\ge M}=\varnothing$$
2	1	adantl	$$⊢\left({\mathbb{Z}}_{\ge M}\ne \varnothing \wedge \neg M\in \mathbb{Z}\right)\to {\mathbb{Z}}_{\ge M}=\varnothing$$
3		neneq	$$⊢{\mathbb{Z}}_{\ge M}\ne \varnothing \to \neg {\mathbb{Z}}_{\ge M}=\varnothing$$
4	3	adantr	$$⊢\left({\mathbb{Z}}_{\ge M}\ne \varnothing \wedge \neg M\in \mathbb{Z}\right)\to \neg {\mathbb{Z}}_{\ge M}=\varnothing$$
5	2 4	condan	$$⊢{\mathbb{Z}}_{\ge M}\ne \varnothing \to M\in \mathbb{Z}$$
6		id	$$⊢M\in \mathbb{Z}\to M\in \mathbb{Z}$$
7		eqid	$$⊢{\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}$$
8	6 7	uzn0d	$$⊢M\in \mathbb{Z}\to {\mathbb{Z}}_{\ge M}\ne \varnothing$$
9	5 8	impbii	$$⊢{\mathbb{Z}}_{\ge M}\ne \varnothing \leftrightarrow M\in \mathbb{Z}$$