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 N3N

Proof

Step Hyp Ref Expression
1 1z 1
2 1le3 13
3 eluzuzle 113N3N1
4 1 2 3 mp2an N3N1
5 elnnuz NN1
6 4 5 sylibr N3N