Theorem uz0

Description: The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	uz0	$$⊢\neg M\in \mathbb{Z}\to {\mathbb{Z}}_{\ge M}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dmuz	$$⊢\mathrm{dom}{\mathbb{Z}}_{\ge }=\mathbb{Z}$$
2	1	eqcomi	$$⊢\mathbb{Z}=\mathrm{dom}{\mathbb{Z}}_{\ge }$$
3	2	eleq2i	$$⊢M\in \mathbb{Z}\leftrightarrow M\in \mathrm{dom}{\mathbb{Z}}_{\ge }$$
4	3	notbii	$$⊢\neg M\in \mathbb{Z}\leftrightarrow \neg M\in \mathrm{dom}{\mathbb{Z}}_{\ge }$$
5	4	biimpi	$$⊢\neg M\in \mathbb{Z}\to \neg M\in \mathrm{dom}{\mathbb{Z}}_{\ge }$$
6		ndmfv	$$⊢\neg M\in \mathrm{dom}{\mathbb{Z}}_{\ge }\to {\mathbb{Z}}_{\ge M}=\varnothing$$
7	5 6	syl	$$⊢\neg M\in \mathbb{Z}\to {\mathbb{Z}}_{\ge M}=\varnothing$$