Theorem zabscl

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

	Ref	Expression
Assertion	zabscl	⊢ ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		nn0abscl	⊢ ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℕ0 )
2	1	nn0zd	⊢ ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℤ )