# Metamath Proof Explorer

## Theorem 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}=\left\{{n}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}{n}={{x}}^{2}+{{y}}^{2}+{{z}}^{2}+{{w}}^{2}\right\}$
Assertion mul4sq ${⊢}\left({A}\in {S}\wedge {B}\in {S}\right)\to {A}{B}\in {S}$

### Proof

Step Hyp Ref Expression
1 4sq.1 ${⊢}{S}=\left\{{n}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}{n}={{x}}^{2}+{{y}}^{2}+{{z}}^{2}+{{w}}^{2}\right\}$
2 1 4sqlem4 ${⊢}{A}\in {S}↔\exists {a}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}$
3 1 4sqlem4 ${⊢}{B}\in {S}↔\exists {c}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}$
4 reeanv ${⊢}\exists {a}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {c}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge \exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)↔\left(\exists {a}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge \exists {c}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)$
5 reeanv ${⊢}\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\left({A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge {B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)↔\left(\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge \exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)$
6 simpll ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {a}\in ℤ\left[i\right]$
7 gzabssqcl ${⊢}{a}\in ℤ\left[i\right]\to {\left|{a}\right|}^{2}\in {ℕ}_{0}$
8 6 7 syl ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {\left|{a}\right|}^{2}\in {ℕ}_{0}$
9 simprl ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {b}\in ℤ\left[i\right]$
10 gzabssqcl ${⊢}{b}\in ℤ\left[i\right]\to {\left|{b}\right|}^{2}\in {ℕ}_{0}$
11 9 10 syl ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {\left|{b}\right|}^{2}\in {ℕ}_{0}$
12 8 11 nn0addcld ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\in {ℕ}_{0}$
13 12 nn0cnd ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\in ℂ$
14 13 div1d ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \frac{{\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}}{1}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}$
15 simplr ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {c}\in ℤ\left[i\right]$
16 gzabssqcl ${⊢}{c}\in ℤ\left[i\right]\to {\left|{c}\right|}^{2}\in {ℕ}_{0}$
17 15 16 syl ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {\left|{c}\right|}^{2}\in {ℕ}_{0}$
18 simprr ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {d}\in ℤ\left[i\right]$
19 gzabssqcl ${⊢}{d}\in ℤ\left[i\right]\to {\left|{d}\right|}^{2}\in {ℕ}_{0}$
20 18 19 syl ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {\left|{d}\right|}^{2}\in {ℕ}_{0}$
21 17 20 nn0addcld ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\in {ℕ}_{0}$
22 21 nn0cnd ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\in ℂ$
23 22 div1d ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \frac{{\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}}{1}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}$
24 14 23 oveq12d ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \left(\frac{{\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}}{1}\right)\left(\frac{{\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}}{1}\right)=\left({\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\right)\left({\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)$
25 eqid ${⊢}{\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}$
26 eqid ${⊢}{\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}$
27 1nn ${⊢}1\in ℕ$
28 27 a1i ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to 1\in ℕ$
29 gzsubcl ${⊢}\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\to {a}-{c}\in ℤ\left[i\right]$
30 29 adantr ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {a}-{c}\in ℤ\left[i\right]$
31 gzcn ${⊢}{a}-{c}\in ℤ\left[i\right]\to {a}-{c}\in ℂ$
32 30 31 syl ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {a}-{c}\in ℂ$
33 32 div1d ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \frac{{a}-{c}}{1}={a}-{c}$
34 33 30 eqeltrd ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \frac{{a}-{c}}{1}\in ℤ\left[i\right]$
35 gzsubcl ${⊢}\left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\to {b}-{d}\in ℤ\left[i\right]$
36 35 adantl ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {b}-{d}\in ℤ\left[i\right]$
37 gzcn ${⊢}{b}-{d}\in ℤ\left[i\right]\to {b}-{d}\in ℂ$
38 36 37 syl ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to {b}-{d}\in ℂ$
39 38 div1d ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \frac{{b}-{d}}{1}={b}-{d}$
40 39 36 eqeltrd ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \frac{{b}-{d}}{1}\in ℤ\left[i\right]$
41 14 12 eqeltrd ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \frac{{\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}}{1}\in {ℕ}_{0}$
42 1 6 9 15 18 25 26 28 34 40 41 mul4sqlem ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \left(\frac{{\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}}{1}\right)\left(\frac{{\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}}{1}\right)\in {S}$
43 24 42 eqeltrrd ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \left({\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\right)\left({\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\in {S}$
44 oveq12 ${⊢}\left({A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge {B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\to {A}{B}=\left({\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\right)\left({\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)$
45 44 eleq1d ${⊢}\left({A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge {B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\to \left({A}{B}\in {S}↔\left({\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\right)\left({\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\in {S}\right)$
46 43 45 syl5ibrcom ${⊢}\left(\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\wedge \left({b}\in ℤ\left[i\right]\wedge {d}\in ℤ\left[i\right]\right)\right)\to \left(\left({A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge {B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\to {A}{B}\in {S}\right)$
47 46 rexlimdvva ${⊢}\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\to \left(\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\left({A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge {B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\to {A}{B}\in {S}\right)$
48 5 47 syl5bir ${⊢}\left({a}\in ℤ\left[i\right]\wedge {c}\in ℤ\left[i\right]\right)\to \left(\left(\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge \exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\to {A}{B}\in {S}\right)$
49 48 rexlimivv ${⊢}\exists {a}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {c}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge \exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\to {A}{B}\in {S}$
50 4 49 sylbir ${⊢}\left(\exists {a}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{A}={\left|{a}\right|}^{2}+{\left|{b}\right|}^{2}\wedge \exists {c}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{B}={\left|{c}\right|}^{2}+{\left|{d}\right|}^{2}\right)\to {A}{B}\in {S}$
51 2 3 50 syl2anb ${⊢}\left({A}\in {S}\wedge {B}\in {S}\right)\to {A}{B}\in {S}$