Theorem zsqcl2

Description: The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014) (Revised by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	zsqcl2	|- ( A e. ZZ -> ( A ^ 2 ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		zsqcl	|- ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
2		zre	|- ( A e. ZZ -> A e. RR )
3		sqge0	|- ( A e. RR -> 0 <_ ( A ^ 2 ) )
4	2 3	syl	|- ( A e. ZZ -> 0 <_ ( A ^ 2 ) )
5		elnn0z	|- ( ( A ^ 2 ) e. NN0 <-> ( ( A ^ 2 ) e. ZZ /\ 0 <_ ( A ^ 2 ) ) )
6	1 4 5	sylanbrc	|- ( A e. ZZ -> ( A ^ 2 ) e. NN0 )