4sqlem4a

		Ref	Expression
	Hypothesis	4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
	Assertion	4sqlem4a	$⊢ (A \in ℤ [i] \land B \in ℤ [i]) \to {\|A\|}^{2} + {\|B\|}^{2} \in S$

Step	Hyp	Ref	Expression
1		4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
2		gzcn	$⊢ A \in ℤ [i] \to A \in ℂ$
3	2	absvalsq2d	$⊢ A \in ℤ [i] \to {\|A\|}^{2} = {ℜ (A)}^{2} + {ℑ (A)}^{2}$
4		gzcn	$⊢ B \in ℤ [i] \to B \in ℂ$
5	4	absvalsq2d	$⊢ B \in ℤ [i] \to {\|B\|}^{2} = {ℜ (B)}^{2} + {ℑ (B)}^{2}$
6	3 5	oveqan12d	$⊢ (A \in ℤ [i] \land B \in ℤ [i]) \to {\|A\|}^{2} + {\|B\|}^{2} = {ℜ (A)}^{2} + {ℑ (A)}^{2} + {ℜ (B)}^{2} + {ℑ (B)}^{2}$
7		elgz	$⊢ A \in ℤ [i] \leftrightarrow (A \in ℂ \land ℜ (A) \in ℤ \land ℑ (A) \in ℤ)$
8	7	simp2bi	$⊢ A \in ℤ [i] \to ℜ (A) \in ℤ$
9	7	simp3bi	$⊢ A \in ℤ [i] \to ℑ (A) \in ℤ$
10	8 9	jca	$⊢ A \in ℤ [i] \to (ℜ (A) \in ℤ \land ℑ (A) \in ℤ)$
11		elgz	$⊢ B \in ℤ [i] \leftrightarrow (B \in ℂ \land ℜ (B) \in ℤ \land ℑ (B) \in ℤ)$
12	11	simp2bi	$⊢ B \in ℤ [i] \to ℜ (B) \in ℤ$
13	11	simp3bi	$⊢ B \in ℤ [i] \to ℑ (B) \in ℤ$
14	12 13	jca	$⊢ B \in ℤ [i] \to (ℜ (B) \in ℤ \land ℑ (B) \in ℤ)$
15	1	4sqlem3	$⊢ ((ℜ (A) \in ℤ \land ℑ (A) \in ℤ) \land (ℜ (B) \in ℤ \land ℑ (B) \in ℤ)) \to {ℜ (A)}^{2} + {ℑ (A)}^{2} + {ℜ (B)}^{2} + {ℑ (B)}^{2} \in S$
16	10 14 15	syl2an	$⊢ (A \in ℤ [i] \land B \in ℤ [i]) \to {ℜ (A)}^{2} + {ℑ (A)}^{2} + {ℜ (B)}^{2} + {ℑ (B)}^{2} \in S$
17	6 16	eqeltrd	$⊢ (A \in ℤ [i] \land B \in ℤ [i]) \to {\|A\|}^{2} + {\|B\|}^{2} \in S$

Metamath Proof Explorer