Metamath Proof Explorer

Theorem eluz5nn

Description: An integer greater than or equal to 5 is a positive integer. (Contributed by AV, 22-Nov-2025)

Ref Expression
Assertion eluz5nn 
|- ( N e. ( ZZ>= ` 5 ) -> N e. NN )

Proof

Step Hyp Ref Expression
1 uzuzle35 
 |-  ( N e. ( ZZ>= ` 5 ) -> N e. ( ZZ>= ` 3 ) )
2 eluz3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
3 1 2 syl 
 |-  ( N e. ( ZZ>= ` 5 ) -> N e. NN )