Metamath Proof Explorer


Theorem zabscl

Description: The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014)

Ref Expression
Assertion zabscl ⊢ A ∈ ℤ → A ∈ ℤ

Proof

Step Hyp Ref Expression
1 nn0abscl ⊢ A ∈ ℤ → A ∈ ℕ 0
2 1 nn0zd ⊢ A ∈ ℤ → A ∈ ℤ