This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∈ ℕ )