msqznn

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

		Ref	Expression
	Assertion	msqznn	$⊢ (A \in ℤ \land A \neq 0) \to A A \in ℕ$

Step	Hyp	Ref	Expression
1		zmulcl	$⊢ (A \in ℤ \land A \in ℤ) \to A A \in ℤ$
2	1	anidms	$⊢ A \in ℤ \to A A \in ℤ$
3	2	adantr	$⊢ (A \in ℤ \land A \neq 0) \to A A \in ℤ$
4		zre	$⊢ A \in ℤ \to A \in ℝ$
5		msqgt0	$⊢ (A \in ℝ \land A \neq 0) \to 0 < A A$
6	4 5	sylan	$⊢ (A \in ℤ \land A \neq 0) \to 0 < A A$
7		elnnz	$⊢ A A \in ℕ \leftrightarrow (A A \in ℤ \land 0 < A A)$
8	3 6 7	sylanbrc	$⊢ (A \in ℤ \land A \neq 0) \to A A \in ℕ$

Metamath Proof Explorer