Metamath Proof Explorer

Theorem eluz2nn

Description: An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018)

Ref Expression
Assertion eluz2nn 
|- ( A e. ( ZZ>= ` 2 ) -> A e. NN )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 1le2 
 |-  1 <_ 2
3 eluzuzle 
 |-  ( ( 1 e. ZZ /\ 1 <_ 2 ) -> ( A e. ( ZZ>= ` 2 ) -> A e. ( ZZ>= ` 1 ) ) )
4 1 2 3 mp2an 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ( ZZ>= ` 1 ) )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 4 5 eleqtrrdi 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )