Metamath Proof Explorer

Theorem 2eluzge1

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

Ref Expression
Assertion 2eluzge1 
|- 2 e. ( ZZ>= ` 1 )

Proof

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