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	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
2		sqval	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
4		nnmulcl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 · 𝐴 ) ∈ ℕ )
5	4	anidms	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 · 𝐴 ) ∈ ℕ )
6	3 5	eqeltrd	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) ∈ ℕ )