Theorem 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 \mathbb{Z}\left[i\right]\to {\left|A\right|}^2\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		gzcn	$$⊢A\in \mathbb{Z}\left[i\right]\to A\in ℂ$$
2	1	absvalsq2d	$$⊢A\in \mathbb{Z}\left[i\right]\to {\left|A\right|}^2={\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
3		elgz	$$⊢A\in \mathbb{Z}\left[i\right]\leftrightarrow \left(A\in ℂ\wedge \Re \left(A\right)\in \mathbb{Z}\wedge \Im \left(A\right)\in \mathbb{Z}\right)$$
4	3	simp2bi	$$⊢A\in \mathbb{Z}\left[i\right]\to \Re \left(A\right)\in \mathbb{Z}$$
5		zsqcl2	$$⊢\Re \left(A\right)\in \mathbb{Z}\to {\Re \left(A\right)}^2\in {\mathbb{N}}_0$$
6	4 5	syl	$$⊢A\in \mathbb{Z}\left[i\right]\to {\Re \left(A\right)}^2\in {\mathbb{N}}_0$$
7	3	simp3bi	$$⊢A\in \mathbb{Z}\left[i\right]\to \Im \left(A\right)\in \mathbb{Z}$$
8		zsqcl2	$$⊢\Im \left(A\right)\in \mathbb{Z}\to {\Im \left(A\right)}^2\in {\mathbb{N}}_0$$
9	7 8	syl	$$⊢A\in \mathbb{Z}\left[i\right]\to {\Im \left(A\right)}^2\in {\mathbb{N}}_0$$
10	6 9	nn0addcld	$$⊢A\in \mathbb{Z}\left[i\right]\to {\Re \left(A\right)}^2+{\Im \left(A\right)}^2\in {\mathbb{N}}_0$$
11	2 10	eqeltrd	$$⊢A\in \mathbb{Z}\left[i\right]\to {\left|A\right|}^2\in {\mathbb{N}}_0$$