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	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	znsqcld.2	⊢ ( 𝜑 → 𝑁 ≠ 0 )
Assertion	znsqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		znsqcld.1	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
2		znsqcld.2	⊢ ( 𝜑 → 𝑁 ≠ 0 )
3	1	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
4		2z	⊢ 2 ∈ ℤ
5	4	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
6	3 2 5	expne0d	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ≠ 0 )
7	6	neneqd	⊢ ( 𝜑 → ¬ ( 𝑁 ↑ 2 ) = 0 )
8		zsqcl2	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ↑ 2 ) ∈ ℕ0 )
9	1 8	syl	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ0 )
10		elnn0	⊢ ( ( 𝑁 ↑ 2 ) ∈ ℕ0 ↔ ( ( 𝑁 ↑ 2 ) ∈ ℕ ∨ ( 𝑁 ↑ 2 ) = 0 ) )
11	9 10	sylib	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) ∈ ℕ ∨ ( 𝑁 ↑ 2 ) = 0 ) )
12	11	orcomd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) = 0 ∨ ( 𝑁 ↑ 2 ) ∈ ℕ ) )
13	12	ord	⊢ ( 𝜑 → ( ¬ ( 𝑁 ↑ 2 ) = 0 → ( 𝑁 ↑ 2 ) ∈ ℕ ) )
14	7 13	mpd	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )