Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 nn0expcl 
 |-  ( ( A e. NN0 /\ 2 e. NN0 ) -> ( A ^ 2 ) e. NN0 )
3 1 2 mpan2 
 |-  ( A e. NN0 -> ( A ^ 2 ) e. NN0 )