Theorem nn0sqcl

Description: The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014)

	Ref	Expression
Assertion	nn0sqcl	$$⊢A\in {\mathbb{N}}_0\to A^2\in {\mathbb{N}}_0$$

Proof

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