Theorem msqznn

Description: The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004)

	Ref	Expression
Assertion	msqznn	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · 𝐴 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		zmulcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 · 𝐴 ) ∈ ℤ )
2	1	anidms	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 · 𝐴 ) ∈ ℤ )
3	2	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · 𝐴 ) ∈ ℤ )
4		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
5		msqgt0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 · 𝐴 ) )
6	4 5	sylan	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 · 𝐴 ) )
7		elnnz	⊢ ( ( 𝐴 · 𝐴 ) ∈ ℕ ↔ ( ( 𝐴 · 𝐴 ) ∈ ℤ ∧ 0 < ( 𝐴 · 𝐴 ) ) )
8	3 6 7	sylanbrc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · 𝐴 ) ∈ ℕ )