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 ) → 𝑁 ∈ ℕ ) |
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 ) → 𝑁 ∈ ℕ ) |