Theorem zsqcl

Description: Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	zsqcl	$$⊢A\in \mathbb{Z}\to A^2\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		zexpcl	$$⊢\left(A\in \mathbb{Z}\wedge 2\in {\mathbb{N}}_0\right)\to A^2\in \mathbb{Z}$$
3	1 2	mpan2	$$⊢A\in \mathbb{Z}\to A^2\in \mathbb{Z}$$