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 ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℕ )

Proof

Step Hyp Ref Expression
1 1z 1 ∈ ℤ
2 1le3 1 ≤ 3
3 eluzuzle ( ( 1 ∈ ℤ ∧ 1 ≤ 3 ) → ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ( ℤ ‘ 1 ) ) )
4 1 2 3 mp2an ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ( ℤ ‘ 1 ) )
5 elnnuz ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ ‘ 1 ) )
6 4 5 sylibr ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℕ )