gzabssqcl

Description: The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014)

		Ref	Expression
	Assertion	gzabssqcl	$⊢ A \in ℤ [i] \to {\|A\|}^{2} \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		gzcn	$⊢ A \in ℤ [i] \to A \in ℂ$
2	1	absvalsq2d	$⊢ A \in ℤ [i] \to {\|A\|}^{2} = {ℜ (A)}^{2} + {ℑ (A)}^{2}$
3		elgz	$⊢ A \in ℤ [i] \leftrightarrow (A \in ℂ \land ℜ (A) \in ℤ \land ℑ (A) \in ℤ)$
4	3	simp2bi	$⊢ A \in ℤ [i] \to ℜ (A) \in ℤ$
5		zsqcl2	$⊢ ℜ (A) \in ℤ \to {ℜ (A)}^{2} \in ℕ_{0}$
6	4 5	syl	$⊢ A \in ℤ [i] \to {ℜ (A)}^{2} \in ℕ_{0}$
7	3	simp3bi	$⊢ A \in ℤ [i] \to ℑ (A) \in ℤ$
8		zsqcl2	$⊢ ℑ (A) \in ℤ \to {ℑ (A)}^{2} \in ℕ_{0}$
9	7 8	syl	$⊢ A \in ℤ [i] \to {ℑ (A)}^{2} \in ℕ_{0}$
10	6 9	nn0addcld	$⊢ A \in ℤ [i] \to {ℜ (A)}^{2} + {ℑ (A)}^{2} \in ℕ_{0}$
11	2 10	eqeltrd	$⊢ A \in ℤ [i] \to {\|A\|}^{2} \in ℕ_{0}$

Metamath Proof Explorer