2sqlem2

		Ref	Expression
	Hypothesis	2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
	Assertion	2sqlem2	$⊢ A \in S \leftrightarrow \exists x \in ℤ \exists y \in ℤ A = x^{2} + y^{2}$

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2	1	2sqlem1	$⊢ A \in S \leftrightarrow \exists z \in ℤ [i] A = {\|z\|}^{2}$
3		elgz	$⊢ z \in ℤ [i] \leftrightarrow (z \in ℂ \land ℜ (z) \in ℤ \land ℑ (z) \in ℤ)$
4	3	simp2bi	$⊢ z \in ℤ [i] \to ℜ (z) \in ℤ$
5	3	simp3bi	$⊢ z \in ℤ [i] \to ℑ (z) \in ℤ$
6		gzcn	$⊢ z \in ℤ [i] \to z \in ℂ$
7	6	absvalsq2d	$⊢ z \in ℤ [i] \to {\|z\|}^{2} = {ℜ (z)}^{2} + {ℑ (z)}^{2}$
8		oveq1	$⊢ x = ℜ (z) \to x^{2} = {ℜ (z)}^{2}$
9	8	oveq1d	$⊢ x = ℜ (z) \to x^{2} + y^{2} = {ℜ (z)}^{2} + y^{2}$
10	9	eqeq2d	$⊢ x = ℜ (z) \to ({\|z\|}^{2} = x^{2} + y^{2} \leftrightarrow {\|z\|}^{2} = {ℜ (z)}^{2} + y^{2})$
11		oveq1	$⊢ y = ℑ (z) \to y^{2} = {ℑ (z)}^{2}$
12	11	oveq2d	$⊢ y = ℑ (z) \to {ℜ (z)}^{2} + y^{2} = {ℜ (z)}^{2} + {ℑ (z)}^{2}$
13	12	eqeq2d	$⊢ y = ℑ (z) \to ({\|z\|}^{2} = {ℜ (z)}^{2} + y^{2} \leftrightarrow {\|z\|}^{2} = {ℜ (z)}^{2} + {ℑ (z)}^{2})$
14	10 13	rspc2ev	$⊢ (ℜ (z) \in ℤ \land ℑ (z) \in ℤ \land {\|z\|}^{2} = {ℜ (z)}^{2} + {ℑ (z)}^{2}) \to \exists x \in ℤ \exists y \in ℤ {\|z\|}^{2} = x^{2} + y^{2}$
15	4 5 7 14	syl3anc	$⊢ z \in ℤ [i] \to \exists x \in ℤ \exists y \in ℤ {\|z\|}^{2} = x^{2} + y^{2}$
16		eqeq1	$⊢ A = {\|z\|}^{2} \to (A = x^{2} + y^{2} \leftrightarrow {\|z\|}^{2} = x^{2} + y^{2})$
17	16	2rexbidv	$⊢ A = {\|z\|}^{2} \to (\exists x \in ℤ \exists y \in ℤ A = x^{2} + y^{2} \leftrightarrow \exists x \in ℤ \exists y \in ℤ {\|z\|}^{2} = x^{2} + y^{2})$
18	15 17	syl5ibrcom	$⊢ z \in ℤ [i] \to (A = {\|z\|}^{2} \to \exists x \in ℤ \exists y \in ℤ A = x^{2} + y^{2})$
19	18	rexlimiv	$⊢ \exists z \in ℤ [i] A = {\|z\|}^{2} \to \exists x \in ℤ \exists y \in ℤ A = x^{2} + y^{2}$
20	2 19	sylbi	$⊢ A \in S \to \exists x \in ℤ \exists y \in ℤ A = x^{2} + y^{2}$
21		gzreim	$⊢ (x \in ℤ \land y \in ℤ) \to x + i y \in ℤ [i]$
22		zcn	$⊢ x \in ℤ \to x \in ℂ$
23		ax-icn	$⊢ i \in ℂ$
24		zcn	$⊢ y \in ℤ \to y \in ℂ$
25		mulcl	$⊢ (i \in ℂ \land y \in ℂ) \to i y \in ℂ$
26	23 24 25	sylancr	$⊢ y \in ℤ \to i y \in ℂ$
27		addcl	$⊢ (x \in ℂ \land i y \in ℂ) \to x + i y \in ℂ$
28	22 26 27	syl2an	$⊢ (x \in ℤ \land y \in ℤ) \to x + i y \in ℂ$
29	28	absvalsq2d	$⊢ (x \in ℤ \land y \in ℤ) \to {\|x + i y\|}^{2} = {ℜ (x + i y)}^{2} + {ℑ (x + i y)}^{2}$
30		zre	$⊢ x \in ℤ \to x \in ℝ$
31		zre	$⊢ y \in ℤ \to y \in ℝ$
32		crre	$⊢ (x \in ℝ \land y \in ℝ) \to ℜ (x + i y) = x$
33	30 31 32	syl2an	$⊢ (x \in ℤ \land y \in ℤ) \to ℜ (x + i y) = x$
34	33	oveq1d	$⊢ (x \in ℤ \land y \in ℤ) \to {ℜ (x + i y)}^{2} = x^{2}$
35		crim	$⊢ (x \in ℝ \land y \in ℝ) \to ℑ (x + i y) = y$
36	30 31 35	syl2an	$⊢ (x \in ℤ \land y \in ℤ) \to ℑ (x + i y) = y$
37	36	oveq1d	$⊢ (x \in ℤ \land y \in ℤ) \to {ℑ (x + i y)}^{2} = y^{2}$
38	34 37	oveq12d	$⊢ (x \in ℤ \land y \in ℤ) \to {ℜ (x + i y)}^{2} + {ℑ (x + i y)}^{2} = x^{2} + y^{2}$
39	29 38	eqtr2d	$⊢ (x \in ℤ \land y \in ℤ) \to x^{2} + y^{2} = {\|x + i y\|}^{2}$
40		fveq2	$⊢ z = x + i y \to \|z\| = \|x + i y\|$
41	40	oveq1d	$⊢ z = x + i y \to {\|z\|}^{2} = {\|x + i y\|}^{2}$
42	41	rspceeqv	$⊢ (x + i y \in ℤ [i] \land x^{2} + y^{2} = {\|x + i y\|}^{2}) \to \exists z \in ℤ [i] x^{2} + y^{2} = {\|z\|}^{2}$
43	21 39 42	syl2anc	$⊢ (x \in ℤ \land y \in ℤ) \to \exists z \in ℤ [i] x^{2} + y^{2} = {\|z\|}^{2}$
44	1	2sqlem1	$⊢ x^{2} + y^{2} \in S \leftrightarrow \exists z \in ℤ [i] x^{2} + y^{2} = {\|z\|}^{2}$
45	43 44	sylibr	$⊢ (x \in ℤ \land y \in ℤ) \to x^{2} + y^{2} \in S$
46		eleq1	$⊢ A = x^{2} + y^{2} \to (A \in S \leftrightarrow x^{2} + y^{2} \in S)$
47	45 46	syl5ibrcom	$⊢ (x \in ℤ \land y \in ℤ) \to (A = x^{2} + y^{2} \to A \in S)$
48	47	rexlimivv	$⊢ \exists x \in ℤ \exists y \in ℤ A = x^{2} + y^{2} \to A \in S$
49	20 48	impbii	$⊢ A \in S \leftrightarrow \exists x \in ℤ \exists y \in ℤ A = x^{2} + y^{2}$

Metamath Proof Explorer

Theorem 2sqlem2

Proof