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

Proof

Step	Hyp	Ref	Expression
1		uz0	|- ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
2	1	adantl	|- ( ( ( ZZ>= ` M ) =/= (/) /\ -. M e. ZZ ) -> ( ZZ>= ` M ) = (/) )
3		neneq	|- ( ( ZZ>= ` M ) =/= (/) -> -. ( ZZ>= ` M ) = (/) )
4	3	adantr	|- ( ( ( ZZ>= ` M ) =/= (/) /\ -. M e. ZZ ) -> -. ( ZZ>= ` M ) = (/) )
5	2 4	condan	|- ( ( ZZ>= ` M ) =/= (/) -> M e. ZZ )
6		id	|- ( M e. ZZ -> M e. ZZ )
7		eqid	|- ( ZZ>= ` M ) = ( ZZ>= ` M )
8	6 7	uzn0d	|- ( M e. ZZ -> ( ZZ>= ` M ) =/= (/) )
9	5 8	impbii	|- ( ( ZZ>= ` M ) =/= (/) <-> M e. ZZ )