Metamath Proof Explorer

Theorem elnnz1

Description: Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion elnnz1 ⊢N∈ℕ↔N∈ℤ∧1≤N

Proof

Step Hyp Ref Expression
1 nnz ⊢N∈ℕ→N∈ℤ
2 nnge1 ⊢N∈ℕ→1≤N
3 1 2 jca ⊢N∈ℕ→N∈ℤ∧1≤N
4 0lt1 ⊢0<1
5 0re ⊢0∈ℝ
6 1re ⊢1∈ℝ
7 zre ⊢N∈ℤ→N∈ℝ
8 ltletr ⊢0∈ℝ∧1∈ℝ∧N∈ℝ→0<1∧1≤N→0<N
9 5 6 7 8 mp3an12i ⊢N∈ℤ→0<1∧1≤N→0<N
10 4 9 mpani ⊢N∈ℤ→1≤N→0<N
11 10 imdistani ⊢N∈ℤ∧1≤N→N∈ℤ∧0<N
12 elnnz ⊢N∈ℕ↔N∈ℤ∧0<N
13 11 12 sylibr ⊢N∈ℤ∧1≤N→N∈ℕ
14 3 13 impbii ⊢N∈ℕ↔N∈ℤ∧1≤N