Metamath Proof Explorer


Theorem eluzge3nn

Description: If an integer is greater than 3, then it is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018)

Ref Expression
Assertion eluzge3nn
|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )

Proof

Step Hyp Ref Expression
1 1z
 |-  1 e. ZZ
2 1le3
 |-  1 <_ 3
3 eluzuzle
 |-  ( ( 1 e. ZZ /\ 1 <_ 3 ) -> ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 1 ) ) )
4 1 2 3 mp2an
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 1 ) )
5 elnnuz
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
6 4 5 sylibr
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )