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