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	$$⊢\phi \to N\in \mathbb{Z}$$
	znsqcld.2	$$⊢\phi \to N\ne 0$$
Assertion	znsqcld	$$⊢\phi \to N^2\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		znsqcld.1	$$⊢\phi \to N\in \mathbb{Z}$$
2		znsqcld.2	$$⊢\phi \to N\ne 0$$
3	1	zcnd	$$⊢\phi \to N\in ℂ$$
4		2z	$$⊢2\in \mathbb{Z}$$
5	4	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
6	3 2 5	expne0d	$$⊢\phi \to N^2\ne 0$$
7	6	neneqd	$$⊢\phi \to \neg N^2=0$$
8		zsqcl2	$$⊢N\in \mathbb{Z}\to N^2\in {\mathbb{N}}_0$$
9	1 8	syl	$$⊢\phi \to N^2\in {\mathbb{N}}_0$$
10		elnn0	$$⊢N^2\in {\mathbb{N}}_0\leftrightarrow \left(N^2\in \mathbb{N}\vee N^2=0\right)$$
11	9 10	sylib	$$⊢\phi \to \left(N^2\in \mathbb{N}\vee N^2=0\right)$$
12	11	orcomd	$$⊢\phi \to \left(N^2=0\vee N^2\in \mathbb{N}\right)$$
13	12	ord	$$⊢\phi \to \left(\neg N^2=0\to N^2\in \mathbb{N}\right)$$
14	7 13	mpd	$$⊢\phi \to N^2\in \mathbb{N}$$