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	|- ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		dmuz	|- dom ZZ>= = ZZ
2	1	eqcomi	|- ZZ = dom ZZ>=
3	2	eleq2i	|- ( M e. ZZ <-> M e. dom ZZ>= )
4	3	notbii	|- ( -. M e. ZZ <-> -. M e. dom ZZ>= )
5	4	biimpi	|- ( -. M e. ZZ -> -. M e. dom ZZ>= )
6		ndmfv	|- ( -. M e. dom ZZ>= -> ( ZZ>= ` M ) = (/) )
7	5 6	syl	|- ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )