Metamath Proof Explorer

Theorem nn0abscl

Description: The absolute value of an integer is a nonnegative integer. (Contributed by NM, 27-Feb-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion nn0abscl ⊢ A ∈ ℤ → A ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 zre ⊢ A ∈ ℤ → A ∈ ℝ
2 absz ⊢ A ∈ ℝ → A ∈ ℤ ↔ A ∈ ℤ
3 1 2 syl ⊢ A ∈ ℤ → A ∈ ℤ ↔ A ∈ ℤ
4 3 ibi ⊢ A ∈ ℤ → A ∈ ℤ
5 zcn ⊢ A ∈ ℤ → A ∈ ℂ
6 absge0 ⊢ A ∈ ℂ → 0 ≤ A
7 5 6 syl ⊢ A ∈ ℤ → 0 ≤ A
8 elnn0z ⊢ A ∈ ℕ 0 ↔ A ∈ ℤ ∧ 0 ≤ A
9 4 7 8 sylanbrc ⊢ A ∈ ℤ → A ∈ ℕ 0