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 )