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 ) |
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 ) |