znsqcld

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

Step	Hyp	Ref	Expression
1		znsqcld.1	$⊢ φ \to N \in ℤ$
2		znsqcld.2	$⊢ φ \to N \neq 0$
3	1	zcnd	$⊢ φ \to N \in ℂ$
4		2z	$⊢ 2 \in ℤ$
5	4	a1i	$⊢ φ \to 2 \in ℤ$
6	3 2 5	expne0d	$⊢ φ \to N^{2} \neq 0$
7	6	neneqd	$⊢ φ \to \neg N^{2} = 0$
8		zsqcl2	$⊢ N \in ℤ \to N^{2} \in ℕ_{0}$
9	1 8	syl	$⊢ φ \to N^{2} \in ℕ_{0}$
10		elnn0	$⊢ N^{2} \in ℕ_{0} \leftrightarrow (N^{2} \in ℕ \lor N^{2} = 0)$
11	9 10	sylib	$⊢ φ \to (N^{2} \in ℕ \lor N^{2} = 0)$
12	11	orcomd	$⊢ φ \to (N^{2} = 0 \lor N^{2} \in ℕ)$
13	12	ord	$⊢ φ \to (\neg N^{2} = 0 \to N^{2} \in ℕ)$
14	7 13	mpd	$⊢ φ \to N^{2} \in ℕ$

Metamath Proof Explorer