Theorem nnsqcl

Description: The positive naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		nncn	$$⊢A\in \mathbb{N}\to A\in ℂ$$
2		sqval	$$⊢A\in ℂ\to A^2=AA$$
3	1 2	syl	$$⊢A\in \mathbb{N}\to A^2=AA$$
4		nnmulcl	$$⊢\left(A\in \mathbb{N}\wedge A\in \mathbb{N}\right)\to AA\in \mathbb{N}$$
5	4	anidms	$$⊢A\in \mathbb{N}\to AA\in \mathbb{N}$$
6	3 5	eqeltrd	$$⊢A\in \mathbb{N}\to A^2\in \mathbb{N}$$