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	$$⊢A\in \mathbb{Z}\to A^2\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		zsqcl	$$⊢A\in \mathbb{Z}\to A^2\in \mathbb{Z}$$
2		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
3		sqge0	$$⊢A\in ℝ\to 0\le A^2$$
4	2 3	syl	$$⊢A\in \mathbb{Z}\to 0\le A^2$$
5		elnn0z	$$⊢A^2\in {\mathbb{N}}_0\leftrightarrow \left(A^2\in \mathbb{Z}\wedge 0\le A^2\right)$$
6	1 4 5	sylanbrc	$$⊢A\in \mathbb{Z}\to A^2\in {\mathbb{N}}_0$$