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 )