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 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
Assertion mul4sq ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 1 4sqlem4 ⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑎 ∈ ℤ[i] ∃ 𝑏 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) )
3 1 4sqlem4 ⊢ ( 𝐵 ∈ 𝑆 ↔ ∃ 𝑐 ∈ ℤ[i] ∃ 𝑑 ∈ ℤ[i] 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) )
4 reeanv ⊢ ( ∃ 𝑎 ∈ ℤ[i] ∃ 𝑐 ∈ ℤ[i] ( ∃ 𝑏 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ ∃ 𝑑 ∈ ℤ[i] 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) ↔ ( ∃ 𝑎 ∈ ℤ[i] ∃ 𝑏 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ ∃ 𝑐 ∈ ℤ[i] ∃ 𝑑 ∈ ℤ[i] 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) )
5 reeanv ⊢ ( ∃ 𝑏 ∈ ℤ[i] ∃ 𝑑 ∈ ℤ[i] ( 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) ↔ ( ∃ 𝑏 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ ∃ 𝑑 ∈ ℤ[i] 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) )
6 simpll ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → 𝑎 ∈ ℤ[i] )
7 gzabssqcl ⊢ ( 𝑎 ∈ ℤ[i] → ( ( abs ‘ 𝑎 ) ↑ 2 ) ∈ ℕ0 )
8 6 7 syl ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( abs ‘ 𝑎 ) ↑ 2 ) ∈ ℕ0 )
9 simprl ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → 𝑏 ∈ ℤ[i] )
10 gzabssqcl ⊢ ( 𝑏 ∈ ℤ[i] → ( ( abs ‘ 𝑏 ) ↑ 2 ) ∈ ℕ0 )
11 9 10 syl ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( abs ‘ 𝑏 ) ↑ 2 ) ∈ ℕ0 )
12 8 11 nn0addcld ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∈ ℕ0 )
13 12 nn0cnd ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∈ ℂ )
14 13 div1d ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) / 1 ) = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) )
15 simplr ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → 𝑐 ∈ ℤ[i] )
16 gzabssqcl ⊢ ( 𝑐 ∈ ℤ[i] → ( ( abs ‘ 𝑐 ) ↑ 2 ) ∈ ℕ0 )
17 15 16 syl ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( abs ‘ 𝑐 ) ↑ 2 ) ∈ ℕ0 )
18 simprr ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → 𝑑 ∈ ℤ[i] )
19 gzabssqcl ⊢ ( 𝑑 ∈ ℤ[i] → ( ( abs ‘ 𝑑 ) ↑ 2 ) ∈ ℕ0 )
20 18 19 syl ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( abs ‘ 𝑑 ) ↑ 2 ) ∈ ℕ0 )
21 17 20 nn0addcld ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ∈ ℕ0 )
22 21 nn0cnd ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ∈ ℂ )
23 22 div1d ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) / 1 ) = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) )
24 14 23 oveq12d ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) / 1 ) · ( ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) / 1 ) ) = ( ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) · ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) )
25 eqid ⊢ ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) )
26 eqid ⊢ ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) )
27 1nn ⊢ 1 ∈ ℕ
28 27 a1i ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → 1 ∈ ℕ )
29 gzsubcl ⊢ ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) → ( 𝑎 − 𝑐 ) ∈ ℤ[i] )
30 29 adantr ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( 𝑎 − 𝑐 ) ∈ ℤ[i] )
31 gzcn ⊢ ( ( 𝑎 − 𝑐 ) ∈ ℤ[i] → ( 𝑎 − 𝑐 ) ∈ ℂ )
32 30 31 syl ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( 𝑎 − 𝑐 ) ∈ ℂ )
33 32 div1d ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( 𝑎 − 𝑐 ) / 1 ) = ( 𝑎 − 𝑐 ) )
34 33 30 eqeltrd ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( 𝑎 − 𝑐 ) / 1 ) ∈ ℤ[i] )
35 gzsubcl ⊢ ( ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) → ( 𝑏 − 𝑑 ) ∈ ℤ[i] )
36 35 adantl ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( 𝑏 − 𝑑 ) ∈ ℤ[i] )
37 gzcn ⊢ ( ( 𝑏 − 𝑑 ) ∈ ℤ[i] → ( 𝑏 − 𝑑 ) ∈ ℂ )
38 36 37 syl ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( 𝑏 − 𝑑 ) ∈ ℂ )
39 38 div1d ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( 𝑏 − 𝑑 ) / 1 ) = ( 𝑏 − 𝑑 ) )
40 39 36 eqeltrd ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( 𝑏 − 𝑑 ) / 1 ) ∈ ℤ[i] )
41 14 12 eqeltrd ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) / 1 ) ∈ ℕ0 )
42 1 6 9 15 18 25 26 28 34 40 41 mul4sqlem ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) / 1 ) · ( ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) / 1 ) ) ∈ 𝑆 )
43 24 42 eqeltrrd ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) · ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) ∈ 𝑆 )
44 oveq12 ⊢ ( ( 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) → ( 𝐴 · 𝐵 ) = ( ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) · ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) )
45 44 eleq1d ⊢ ( ( 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) → ( ( 𝐴 · 𝐵 ) ∈ 𝑆 ↔ ( ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) · ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) ∈ 𝑆 ) )
46 43 45 syl5ibrcom ⊢ ( ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) ∧ ( 𝑏 ∈ ℤ[i] ∧ 𝑑 ∈ ℤ[i] ) ) → ( ( 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 ) )
47 46 rexlimdvva ⊢ ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) → ( ∃ 𝑏 ∈ ℤ[i] ∃ 𝑑 ∈ ℤ[i] ( 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 ) )
48 5 47 syl5bir ⊢ ( ( 𝑎 ∈ ℤ[i] ∧ 𝑐 ∈ ℤ[i] ) → ( ( ∃ 𝑏 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ ∃ 𝑑 ∈ ℤ[i] 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 ) )
49 48 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤ[i] ∃ 𝑐 ∈ ℤ[i] ( ∃ 𝑏 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ ∃ 𝑑 ∈ ℤ[i] 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 )
50 4 49 sylbir ⊢ ( ( ∃ 𝑎 ∈ ℤ[i] ∃ 𝑏 ∈ ℤ[i] 𝐴 = ( ( ( abs ‘ 𝑎 ) ↑ 2 ) + ( ( abs ‘ 𝑏 ) ↑ 2 ) ) ∧ ∃ 𝑐 ∈ ℤ[i] ∃ 𝑑 ∈ ℤ[i] 𝐵 = ( ( ( abs ‘ 𝑐 ) ↑ 2 ) + ( ( abs ‘ 𝑑 ) ↑ 2 ) ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 )
51 2 3 50 syl2anb ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 )