Theorem msqznn

Description: The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004)

	Ref	Expression
Assertion	msqznn	|- ( ( A e. ZZ /\ A =/= 0 ) -> ( A x. A ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		zmulcl	|- ( ( A e. ZZ /\ A e. ZZ ) -> ( A x. A ) e. ZZ )
2	1	anidms	|- ( A e. ZZ -> ( A x. A ) e. ZZ )
3	2	adantr	|- ( ( A e. ZZ /\ A =/= 0 ) -> ( A x. A ) e. ZZ )
4		zre	|- ( A e. ZZ -> A e. RR )
5		msqgt0	|- ( ( A e. RR /\ A =/= 0 ) -> 0 < ( A x. A ) )
6	4 5	sylan	|- ( ( A e. ZZ /\ A =/= 0 ) -> 0 < ( A x. A ) )
7		elnnz	|- ( ( A x. A ) e. NN <-> ( ( A x. A ) e. ZZ /\ 0 < ( A x. A ) ) )
8	3 6 7	sylanbrc	|- ( ( A e. ZZ /\ A =/= 0 ) -> ( A x. A ) e. NN )