Metamath Proof Explorer

Theorem 1eluzge0

Description: 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Assertion 1eluzge0 
|- 1 e. ( ZZ>= ` 0 )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 1z 
 |-  1 e. ZZ
3 0le1 
 |-  0 <_ 1
4 eluz2 
 |-  ( 1 e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ 1 e. ZZ /\ 0 <_ 1 ) )
5 1 2 3 4 mpbir3an 
 |-  1 e. ( ZZ>= ` 0 )