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	⊢ ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℕ0 )

Proof

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