Metamath Proof Explorer

Theorem uzn0d

Description: The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses uzn0d.1 
|- ( ph -> M e. ZZ )
uzn0d.2 
|- Z = ( ZZ>= ` M )
Assertion uzn0d 
|- ( ph -> Z =/= (/) )

Proof

Step Hyp Ref Expression
1 uzn0d.1 
 |-  ( ph -> M e. ZZ )
2 uzn0d.2 
 |-  Z = ( ZZ>= ` M )
3 1 2 uzidd2 
 |-  ( ph -> M e. Z )
4 3 ne0d 
 |-  ( ph -> Z =/= (/) )