4sqlem4

Description: Lemma for 4sq . We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014)

		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	4sqlem4	$⊢ A \in S \leftrightarrow \exists u \in ℤ [i] \exists v \in ℤ [i] A = {\|u\|}^{2} + {\|v\|}^{2}$

Proof

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	1	4sqlem2	$⊢ A \in S \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2}$
3		gzreim	$⊢ (a \in ℤ \land b \in ℤ) \to a + i b \in ℤ [i]$
4	3	adantr	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \to a + i b \in ℤ [i]$
5		gzreim	$⊢ (c \in ℤ \land d \in ℤ) \to c + i d \in ℤ [i]$
6	5	adantl	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \to c + i d \in ℤ [i]$
7		gzcn	$⊢ a + i b \in ℤ [i] \to a + i b \in ℂ$
8	3 7	syl	$⊢ (a \in ℤ \land b \in ℤ) \to a + i b \in ℂ$
9	8	absvalsq2d	$⊢ (a \in ℤ \land b \in ℤ) \to {\|a + i b\|}^{2} = {ℜ (a + i b)}^{2} + {ℑ (a + i b)}^{2}$
10		zre	$⊢ a \in ℤ \to a \in ℝ$
11		zre	$⊢ b \in ℤ \to b \in ℝ$
12		crre	$⊢ (a \in ℝ \land b \in ℝ) \to ℜ (a + i b) = a$
13	10 11 12	syl2an	$⊢ (a \in ℤ \land b \in ℤ) \to ℜ (a + i b) = a$
14	13	oveq1d	$⊢ (a \in ℤ \land b \in ℤ) \to {ℜ (a + i b)}^{2} = a^{2}$
15		crim	$⊢ (a \in ℝ \land b \in ℝ) \to ℑ (a + i b) = b$
16	10 11 15	syl2an	$⊢ (a \in ℤ \land b \in ℤ) \to ℑ (a + i b) = b$
17	16	oveq1d	$⊢ (a \in ℤ \land b \in ℤ) \to {ℑ (a + i b)}^{2} = b^{2}$
18	14 17	oveq12d	$⊢ (a \in ℤ \land b \in ℤ) \to {ℜ (a + i b)}^{2} + {ℑ (a + i b)}^{2} = a^{2} + b^{2}$
19	9 18	eqtrd	$⊢ (a \in ℤ \land b \in ℤ) \to {\|a + i b\|}^{2} = a^{2} + b^{2}$
20		gzcn	$⊢ c + i d \in ℤ [i] \to c + i d \in ℂ$
21	5 20	syl	$⊢ (c \in ℤ \land d \in ℤ) \to c + i d \in ℂ$
22	21	absvalsq2d	$⊢ (c \in ℤ \land d \in ℤ) \to {\|c + i d\|}^{2} = {ℜ (c + i d)}^{2} + {ℑ (c + i d)}^{2}$
23		zre	$⊢ c \in ℤ \to c \in ℝ$
24		zre	$⊢ d \in ℤ \to d \in ℝ$
25		crre	$⊢ (c \in ℝ \land d \in ℝ) \to ℜ (c + i d) = c$
26	23 24 25	syl2an	$⊢ (c \in ℤ \land d \in ℤ) \to ℜ (c + i d) = c$
27	26	oveq1d	$⊢ (c \in ℤ \land d \in ℤ) \to {ℜ (c + i d)}^{2} = c^{2}$
28		crim	$⊢ (c \in ℝ \land d \in ℝ) \to ℑ (c + i d) = d$
29	23 24 28	syl2an	$⊢ (c \in ℤ \land d \in ℤ) \to ℑ (c + i d) = d$
30	29	oveq1d	$⊢ (c \in ℤ \land d \in ℤ) \to {ℑ (c + i d)}^{2} = d^{2}$
31	27 30	oveq12d	$⊢ (c \in ℤ \land d \in ℤ) \to {ℜ (c + i d)}^{2} + {ℑ (c + i d)}^{2} = c^{2} + d^{2}$
32	22 31	eqtrd	$⊢ (c \in ℤ \land d \in ℤ) \to {\|c + i d\|}^{2} = c^{2} + d^{2}$
33	19 32	oveqan12d	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \to {\|a + i b\|}^{2} + {\|c + i d\|}^{2} = a^{2} + b^{2} + c^{2} + d^{2}$
34	33	eqcomd	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \to a^{2} + b^{2} + c^{2} + d^{2} = {\|a + i b\|}^{2} + {\|c + i d\|}^{2}$
35		fveq2	$⊢ u = a + i b \to \|u\| = \|a + i b\|$
36	35	oveq1d	$⊢ u = a + i b \to {\|u\|}^{2} = {\|a + i b\|}^{2}$
37	36	oveq1d	$⊢ u = a + i b \to {\|u\|}^{2} + {\|v\|}^{2} = {\|a + i b\|}^{2} + {\|v\|}^{2}$
38	37	eqeq2d	$⊢ u = a + i b \to (a^{2} + b^{2} + c^{2} + d^{2} = {\|u\|}^{2} + {\|v\|}^{2} \leftrightarrow a^{2} + b^{2} + c^{2} + d^{2} = {\|a + i b\|}^{2} + {\|v\|}^{2})$
39		fveq2	$⊢ v = c + i d \to \|v\| = \|c + i d\|$
40	39	oveq1d	$⊢ v = c + i d \to {\|v\|}^{2} = {\|c + i d\|}^{2}$
41	40	oveq2d	$⊢ v = c + i d \to {\|a + i b\|}^{2} + {\|v\|}^{2} = {\|a + i b\|}^{2} + {\|c + i d\|}^{2}$
42	41	eqeq2d	$⊢ v = c + i d \to (a^{2} + b^{2} + c^{2} + d^{2} = {\|a + i b\|}^{2} + {\|v\|}^{2} \leftrightarrow a^{2} + b^{2} + c^{2} + d^{2} = {\|a + i b\|}^{2} + {\|c + i d\|}^{2})$
43	38 42	rspc2ev	$⊢ (a + i b \in ℤ [i] \land c + i d \in ℤ [i] \land a^{2} + b^{2} + c^{2} + d^{2} = {\|a + i b\|}^{2} + {\|c + i d\|}^{2}) \to \exists u \in ℤ [i] \exists v \in ℤ [i] a^{2} + b^{2} + c^{2} + d^{2} = {\|u\|}^{2} + {\|v\|}^{2}$
44	4 6 34 43	syl3anc	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \to \exists u \in ℤ [i] \exists v \in ℤ [i] a^{2} + b^{2} + c^{2} + d^{2} = {\|u\|}^{2} + {\|v\|}^{2}$
45		eqeq1	$⊢ A = a^{2} + b^{2} + c^{2} + d^{2} \to (A = {\|u\|}^{2} + {\|v\|}^{2} \leftrightarrow a^{2} + b^{2} + c^{2} + d^{2} = {\|u\|}^{2} + {\|v\|}^{2})$
46	45	2rexbidv	$⊢ A = a^{2} + b^{2} + c^{2} + d^{2} \to (\exists u \in ℤ [i] \exists v \in ℤ [i] A = {\|u\|}^{2} + {\|v\|}^{2} \leftrightarrow \exists u \in ℤ [i] \exists v \in ℤ [i] a^{2} + b^{2} + c^{2} + d^{2} = {\|u\|}^{2} + {\|v\|}^{2})$
47	44 46	syl5ibrcom	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \to (A = a^{2} + b^{2} + c^{2} + d^{2} \to \exists u \in ℤ [i] \exists v \in ℤ [i] A = {\|u\|}^{2} + {\|v\|}^{2})$
48	47	rexlimdvva	$⊢ (a \in ℤ \land b \in ℤ) \to (\exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2} \to \exists u \in ℤ [i] \exists v \in ℤ [i] A = {\|u\|}^{2} + {\|v\|}^{2})$
49	48	rexlimivv	$⊢ \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2} \to \exists u \in ℤ [i] \exists v \in ℤ [i] A = {\|u\|}^{2} + {\|v\|}^{2}$
50	2 49	sylbi	$⊢ A \in S \to \exists u \in ℤ [i] \exists v \in ℤ [i] A = {\|u\|}^{2} + {\|v\|}^{2}$
51	1	4sqlem4a	$⊢ (u \in ℤ [i] \land v \in ℤ [i]) \to {\|u\|}^{2} + {\|v\|}^{2} \in S$
52		eleq1a	$⊢ {\|u\|}^{2} + {\|v\|}^{2} \in S \to (A = {\|u\|}^{2} + {\|v\|}^{2} \to A \in S)$
53	51 52	syl	$⊢ (u \in ℤ [i] \land v \in ℤ [i]) \to (A = {\|u\|}^{2} + {\|v\|}^{2} \to A \in S)$
54	53	rexlimivv	$⊢ \exists u \in ℤ [i] \exists v \in ℤ [i] A = {\|u\|}^{2} + {\|v\|}^{2} \to A \in S$
55	50 54	impbii	$⊢ A \in S \leftrightarrow \exists u \in ℤ [i] \exists v \in ℤ [i] A = {\|u\|}^{2} + {\|v\|}^{2}$

Metamath Proof Explorer

Theorem 4sqlem4

Proof