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 )