Metamath Proof Explorer

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 e. NN -> ( A ^ 2 ) e. NN )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( A e. NN -> A e. CC )
2 sqval 
 |-  ( A e. CC -> ( A ^ 2 ) = ( A x. A ) )
3 1 2 syl 
 |-  ( A e. NN -> ( A ^ 2 ) = ( A x. A ) )
4 nnmulcl 
 |-  ( ( A e. NN /\ A e. NN ) -> ( A x. A ) e. NN )
5 4 anidms 
 |-  ( A e. NN -> ( A x. A ) e. NN )
6 3 5 eqeltrd 
 |-  ( A e. NN -> ( A ^ 2 ) e. NN )