Metamath Proof Explorer

Theorem 2eluzge0

Description: 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018) (Proof shortened by OpenAI, 25-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 1 2 eleqtri 
 |-  2 e. ( ZZ>= ` 0 )