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

Proof

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