Metamath Proof Explorer

Theorem eluz4nn

Description: An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023)

Ref Expression
Assertion eluz4nn 
|- ( X e. ( ZZ>= ` 4 ) -> X e. NN )

Proof

Step Hyp Ref Expression
1 eluz4eluz2 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 2 ) )
2 eluz2nn 
 |-  ( X e. ( ZZ>= ` 2 ) -> X e. NN )
3 1 2 syl 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. NN )