Metamath Proof Explorer

Theorem nnabscl

Description: The absolute value of a nonzero integer is a positive integer. (Contributed by Paul Chapman, 21-Mar-2011) (Proof shortened by Andrew Salmon, 25-May-2011)

Ref Expression
Assertion nnabscl ⊢ N ∈ ℤ ∧ N ≠ 0 → N ∈ ℕ

Proof

Step Hyp Ref Expression
1 zabscl ⊢ N ∈ ℤ → N ∈ ℤ
2 1 adantr ⊢ N ∈ ℤ ∧ N ≠ 0 → N ∈ ℤ
3 zcn ⊢ N ∈ ℤ → N ∈ ℂ
4 absgt0 ⊢ N ∈ ℂ → N ≠ 0 ↔ 0 < N
5 3 4 syl ⊢ N ∈ ℤ → N ≠ 0 ↔ 0 < N
6 5 biimpa ⊢ N ∈ ℤ ∧ N ≠ 0 → 0 < N
7 elnnz ⊢ N ∈ ℕ ↔ N ∈ ℤ ∧ 0 < N
8 2 6 7 sylanbrc ⊢ N ∈ ℤ ∧ N ≠ 0 → N ∈ ℕ