mul4sq

Description: Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem . (For the curious, the explicit formula that is used is ( | a | ^ 2 + | b | ^ 2 ) ( | c | ^ 2 + | d | ^ 2 ) = | a * x. c + b x. d * | ^ 2 + | a * x. d - b x. c * | ^ 2 .) (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	mul4sq	$⊢ (A \in S \land B \in S) \to A B \in S$

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	4sqlem4	$⊢ A \in S \leftrightarrow \exists a \in ℤ [i] \exists b \in ℤ [i] A = {\|a\|}^{2} + {\|b\|}^{2}$
3	1	4sqlem4	$⊢ B \in S \leftrightarrow \exists c \in ℤ [i] \exists d \in ℤ [i] B = {\|c\|}^{2} + {\|d\|}^{2}$
4		reeanv	$⊢ \exists a \in ℤ [i] \exists c \in ℤ [i] (\exists b \in ℤ [i] A = {\|a\|}^{2} + {\|b\|}^{2} \land \exists d \in ℤ [i] B = {\|c\|}^{2} + {\|d\|}^{2}) \leftrightarrow (\exists a \in ℤ [i] \exists b \in ℤ [i] A = {\|a\|}^{2} + {\|b\|}^{2} \land \exists c \in ℤ [i] \exists d \in ℤ [i] B = {\|c\|}^{2} + {\|d\|}^{2})$
5		reeanv	$⊢ \exists b \in ℤ [i] \exists d \in ℤ [i] (A = {\|a\|}^{2} + {\|b\|}^{2} \land B = {\|c\|}^{2} + {\|d\|}^{2}) \leftrightarrow (\exists b \in ℤ [i] A = {\|a\|}^{2} + {\|b\|}^{2} \land \exists d \in ℤ [i] B = {\|c\|}^{2} + {\|d\|}^{2})$
6		simpll	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to a \in ℤ [i]$
7		gzabssqcl	$⊢ a \in ℤ [i] \to {\|a\|}^{2} \in ℕ_{0}$
8	6 7	syl	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to {\|a\|}^{2} \in ℕ_{0}$
9		simprl	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to b \in ℤ [i]$
10		gzabssqcl	$⊢ b \in ℤ [i] \to {\|b\|}^{2} \in ℕ_{0}$
11	9 10	syl	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to {\|b\|}^{2} \in ℕ_{0}$
12	8 11	nn0addcld	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to {\|a\|}^{2} + {\|b\|}^{2} \in ℕ_{0}$
13	12	nn0cnd	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to {\|a\|}^{2} + {\|b\|}^{2} \in ℂ$
14	13	div1d	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to \frac{{\|a\|}^{2} + {\|b\|}^{2}}{1} = {\|a\|}^{2} + {\|b\|}^{2}$
15		simplr	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to c \in ℤ [i]$
16		gzabssqcl	$⊢ c \in ℤ [i] \to {\|c\|}^{2} \in ℕ_{0}$
17	15 16	syl	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to {\|c\|}^{2} \in ℕ_{0}$
18		simprr	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to d \in ℤ [i]$
19		gzabssqcl	$⊢ d \in ℤ [i] \to {\|d\|}^{2} \in ℕ_{0}$
20	18 19	syl	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to {\|d\|}^{2} \in ℕ_{0}$
21	17 20	nn0addcld	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to {\|c\|}^{2} + {\|d\|}^{2} \in ℕ_{0}$
22	21	nn0cnd	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to {\|c\|}^{2} + {\|d\|}^{2} \in ℂ$
23	22	div1d	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to \frac{{\|c\|}^{2} + {\|d\|}^{2}}{1} = {\|c\|}^{2} + {\|d\|}^{2}$
24	14 23	oveq12d	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to (\frac{{\|a\|}^{2} + {\|b\|}^{2}}{1}) (\frac{{\|c\|}^{2} + {\|d\|}^{2}}{1}) = ({\|a\|}^{2} + {\|b\|}^{2}) ({\|c\|}^{2} + {\|d\|}^{2})$
25		eqid	$⊢ {\|a\|}^{2} + {\|b\|}^{2} = {\|a\|}^{2} + {\|b\|}^{2}$
26		eqid	$⊢ {\|c\|}^{2} + {\|d\|}^{2} = {\|c\|}^{2} + {\|d\|}^{2}$
27		1nn	$⊢ 1 \in ℕ$
28	27	a1i	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to 1 \in ℕ$
29		gzsubcl	$⊢ (a \in ℤ [i] \land c \in ℤ [i]) \to a - c \in ℤ [i]$
30	29	adantr	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to a - c \in ℤ [i]$
31		gzcn	$⊢ a - c \in ℤ [i] \to a - c \in ℂ$
32	30 31	syl	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to a - c \in ℂ$
33	32	div1d	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to \frac{a - c}{1} = a - c$
34	33 30	eqeltrd	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to \frac{a - c}{1} \in ℤ [i]$
35		gzsubcl	$⊢ (b \in ℤ [i] \land d \in ℤ [i]) \to b - d \in ℤ [i]$
36	35	adantl	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to b - d \in ℤ [i]$
37		gzcn	$⊢ b - d \in ℤ [i] \to b - d \in ℂ$
38	36 37	syl	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to b - d \in ℂ$
39	38	div1d	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to \frac{b - d}{1} = b - d$
40	39 36	eqeltrd	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to \frac{b - d}{1} \in ℤ [i]$
41	14 12	eqeltrd	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to \frac{{\|a\|}^{2} + {\|b\|}^{2}}{1} \in ℕ_{0}$
42	1 6 9 15 18 25 26 28 34 40 41	mul4sqlem	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to (\frac{{\|a\|}^{2} + {\|b\|}^{2}}{1}) (\frac{{\|c\|}^{2} + {\|d\|}^{2}}{1}) \in S$
43	24 42	eqeltrrd	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to ({\|a\|}^{2} + {\|b\|}^{2}) ({\|c\|}^{2} + {\|d\|}^{2}) \in S$
44		oveq12	$⊢ (A = {\|a\|}^{2} + {\|b\|}^{2} \land B = {\|c\|}^{2} + {\|d\|}^{2}) \to A B = ({\|a\|}^{2} + {\|b\|}^{2}) ({\|c\|}^{2} + {\|d\|}^{2})$
45	44	eleq1d	$⊢ (A = {\|a\|}^{2} + {\|b\|}^{2} \land B = {\|c\|}^{2} + {\|d\|}^{2}) \to (A B \in S \leftrightarrow ({\|a\|}^{2} + {\|b\|}^{2}) ({\|c\|}^{2} + {\|d\|}^{2}) \in S)$
46	43 45	syl5ibrcom	$⊢ ((a \in ℤ [i] \land c \in ℤ [i]) \land (b \in ℤ [i] \land d \in ℤ [i])) \to ((A = {\|a\|}^{2} + {\|b\|}^{2} \land B = {\|c\|}^{2} + {\|d\|}^{2}) \to A B \in S)$
47	46	rexlimdvva	$⊢ (a \in ℤ [i] \land c \in ℤ [i]) \to (\exists b \in ℤ [i] \exists d \in ℤ [i] (A = {\|a\|}^{2} + {\|b\|}^{2} \land B = {\|c\|}^{2} + {\|d\|}^{2}) \to A B \in S)$
48	5 47	biimtrrid	$⊢ (a \in ℤ [i] \land c \in ℤ [i]) \to ((\exists b \in ℤ [i] A = {\|a\|}^{2} + {\|b\|}^{2} \land \exists d \in ℤ [i] B = {\|c\|}^{2} + {\|d\|}^{2}) \to A B \in S)$
49	48	rexlimivv	$⊢ \exists a \in ℤ [i] \exists c \in ℤ [i] (\exists b \in ℤ [i] A = {\|a\|}^{2} + {\|b\|}^{2} \land \exists d \in ℤ [i] B = {\|c\|}^{2} + {\|d\|}^{2}) \to A B \in S$
50	4 49	sylbir	$⊢ (\exists a \in ℤ [i] \exists b \in ℤ [i] A = {\|a\|}^{2} + {\|b\|}^{2} \land \exists c \in ℤ [i] \exists d \in ℤ [i] B = {\|c\|}^{2} + {\|d\|}^{2}) \to A B \in S$
51	2 3 50	syl2anb	$⊢ (A \in S \land B \in S) \to A B \in S$

Metamath Proof Explorer

Theorem mul4sq

Proof