Theorem zsqcl2

Description: The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014) (Revised by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	zsqcl2	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		zsqcl	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
2		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
3		sqge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 ↑ 2 ) )
4	2 3	syl	⊢ ( 𝐴 ∈ ℤ → 0 ≤ ( 𝐴 ↑ 2 ) )
5		elnn0z	⊢ ( ( 𝐴 ↑ 2 ) ∈ ℕ0 ↔ ( ( 𝐴 ↑ 2 ) ∈ ℤ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) )
6	1 4 5	sylanbrc	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℕ0 )