This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )