Theorem znsqcld

Description: The square of a nonzero integer is a positive integer. (Contributed by Thierry Arnoux, 2-Feb-2020)

	Ref	Expression
Hypotheses	znsqcld.1	|- ( ph -> N e. ZZ )
	znsqcld.2	|- ( ph -> N =/= 0 )
Assertion	znsqcld	|- ( ph -> ( N ^ 2 ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		znsqcld.1	|- ( ph -> N e. ZZ )
2		znsqcld.2	|- ( ph -> N =/= 0 )
3	1	zcnd	|- ( ph -> N e. CC )
4		2z	|- 2 e. ZZ
5	4	a1i	|- ( ph -> 2 e. ZZ )
6	3 2 5	expne0d	|- ( ph -> ( N ^ 2 ) =/= 0 )
7	6	neneqd	|- ( ph -> -. ( N ^ 2 ) = 0 )
8		zsqcl2	|- ( N e. ZZ -> ( N ^ 2 ) e. NN0 )
9	1 8	syl	|- ( ph -> ( N ^ 2 ) e. NN0 )
10		elnn0	|- ( ( N ^ 2 ) e. NN0 <-> ( ( N ^ 2 ) e. NN \/ ( N ^ 2 ) = 0 ) )
11	9 10	sylib	|- ( ph -> ( ( N ^ 2 ) e. NN \/ ( N ^ 2 ) = 0 ) )
12	11	orcomd	|- ( ph -> ( ( N ^ 2 ) = 0 \/ ( N ^ 2 ) e. NN ) )
13	12	ord	|- ( ph -> ( -. ( N ^ 2 ) = 0 -> ( N ^ 2 ) e. NN ) )
14	7 13	mpd	|- ( ph -> ( N ^ 2 ) e. NN )