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 = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
Assertion mul4sq 
|- ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )

Proof

Step Hyp Ref Expression
1 4sq.1 
 |-  S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
2 1 4sqlem4 
 |-  ( A e. S <-> E. a e. Z[i] E. b e. Z[i] A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) )
3 1 4sqlem4 
 |-  ( B e. S <-> E. c e. Z[i] E. d e. Z[i] B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) )
4 reeanv 
 |-  ( E. a e. Z[i] E. c e. Z[i] ( E. b e. Z[i] A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ E. d e. Z[i] B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) <-> ( E. a e. Z[i] E. b e. Z[i] A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ E. c e. Z[i] E. d e. Z[i] B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) )
5 reeanv 
 |-  ( E. b e. Z[i] E. d e. Z[i] ( A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) <-> ( E. b e. Z[i] A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ E. d e. Z[i] B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) )
6 simpll 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> a e. Z[i] )
7 gzabssqcl 
 |-  ( a e. Z[i] -> ( ( abs ` a ) ^ 2 ) e. NN0 )
8 6 7 syl 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( abs ` a ) ^ 2 ) e. NN0 )
9 simprl 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> b e. Z[i] )
10 gzabssqcl 
 |-  ( b e. Z[i] -> ( ( abs ` b ) ^ 2 ) e. NN0 )
11 9 10 syl 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( abs ` b ) ^ 2 ) e. NN0 )
12 8 11 nn0addcld 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) e. NN0 )
13 12 nn0cnd 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) e. CC )
14 13 div1d 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) / 1 ) = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) )
15 simplr 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> c e. Z[i] )
16 gzabssqcl 
 |-  ( c e. Z[i] -> ( ( abs ` c ) ^ 2 ) e. NN0 )
17 15 16 syl 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( abs ` c ) ^ 2 ) e. NN0 )
18 simprr 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> d e. Z[i] )
19 gzabssqcl 
 |-  ( d e. Z[i] -> ( ( abs ` d ) ^ 2 ) e. NN0 )
20 18 19 syl 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( abs ` d ) ^ 2 ) e. NN0 )
21 17 20 nn0addcld 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) e. NN0 )
22 21 nn0cnd 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) e. CC )
23 22 div1d 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) / 1 ) = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) )
24 14 23 oveq12d 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) / 1 ) x. ( ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) / 1 ) ) = ( ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) x. ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) )
25 eqid 
 |-  ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) )
26 eqid 
 |-  ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) )
27 1nn 
 |-  1 e. NN
28 27 a1i 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> 1 e. NN )
29 gzsubcl 
 |-  ( ( a e. Z[i] /\ c e. Z[i] ) -> ( a - c ) e. Z[i] )
30 29 adantr 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( a - c ) e. Z[i] )
31 gzcn 
 |-  ( ( a - c ) e. Z[i] -> ( a - c ) e. CC )
32 30 31 syl 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( a - c ) e. CC )
33 32 div1d 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( a - c ) / 1 ) = ( a - c ) )
34 33 30 eqeltrd 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( a - c ) / 1 ) e. Z[i] )
35 gzsubcl 
 |-  ( ( b e. Z[i] /\ d e. Z[i] ) -> ( b - d ) e. Z[i] )
36 35 adantl 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( b - d ) e. Z[i] )
37 gzcn 
 |-  ( ( b - d ) e. Z[i] -> ( b - d ) e. CC )
38 36 37 syl 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( b - d ) e. CC )
39 38 div1d 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( b - d ) / 1 ) = ( b - d ) )
40 39 36 eqeltrd 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( b - d ) / 1 ) e. Z[i] )
41 14 12 eqeltrd 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) / 1 ) e. NN0 )
42 1 6 9 15 18 25 26 28 34 40 41 mul4sqlem 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) / 1 ) x. ( ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) / 1 ) ) e. S )
43 24 42 eqeltrrd 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) x. ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) e. S )
44 oveq12 
 |-  ( ( A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) -> ( A x. B ) = ( ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) x. ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) )
45 44 eleq1d 
 |-  ( ( A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) -> ( ( A x. B ) e. S <-> ( ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) x. ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) e. S ) )
46 43 45 syl5ibrcom 
 |-  ( ( ( a e. Z[i] /\ c e. Z[i] ) /\ ( b e. Z[i] /\ d e. Z[i] ) ) -> ( ( A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) -> ( A x. B ) e. S ) )
47 46 rexlimdvva 
 |-  ( ( a e. Z[i] /\ c e. Z[i] ) -> ( E. b e. Z[i] E. d e. Z[i] ( A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) -> ( A x. B ) e. S ) )
48 5 47 syl5bir 
 |-  ( ( a e. Z[i] /\ c e. Z[i] ) -> ( ( E. b e. Z[i] A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ E. d e. Z[i] B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) -> ( A x. B ) e. S ) )
49 48 rexlimivv 
 |-  ( E. a e. Z[i] E. c e. Z[i] ( E. b e. Z[i] A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ E. d e. Z[i] B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) -> ( A x. B ) e. S )
50 4 49 sylbir 
 |-  ( ( E. a e. Z[i] E. b e. Z[i] A = ( ( ( abs ` a ) ^ 2 ) + ( ( abs ` b ) ^ 2 ) ) /\ E. c e. Z[i] E. d e. Z[i] B = ( ( ( abs ` c ) ^ 2 ) + ( ( abs ` d ) ^ 2 ) ) ) -> ( A x. B ) e. S )
51 2 3 50 syl2anb 
 |-  ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )