Metamath Proof Explorer

Theorem mul2sq

Description: Fibonacci's identity (actually due to Diophantus). The product of two sums of two squares is also a sum of two squares. We can take advantage of Gaussian integers here to trivialize the proof. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypothesis 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
Assertion mul2sq 
|- ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )

Proof

Step Hyp Ref Expression
1 2sq.1 
 |-  S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 1 2sqlem1 
 |-  ( A e. S <-> E. x e. Z[i] A = ( ( abs ` x ) ^ 2 ) )
3 1 2sqlem1 
 |-  ( B e. S <-> E. y e. Z[i] B = ( ( abs ` y ) ^ 2 ) )
4 reeanv 
 |-  ( E. x e. Z[i] E. y e. Z[i] ( A = ( ( abs ` x ) ^ 2 ) /\ B = ( ( abs ` y ) ^ 2 ) ) <-> ( E. x e. Z[i] A = ( ( abs ` x ) ^ 2 ) /\ E. y e. Z[i] B = ( ( abs ` y ) ^ 2 ) ) )
5 gzmulcl 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( x x. y ) e. Z[i] )
6 gzcn 
 |-  ( x e. Z[i] -> x e. CC )
7 gzcn 
 |-  ( y e. Z[i] -> y e. CC )
8 absmul 
 |-  ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x x. y ) ) = ( ( abs ` x ) x. ( abs ` y ) ) )
9 6 7 8 syl2an 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( abs ` ( x x. y ) ) = ( ( abs ` x ) x. ( abs ` y ) ) )
10 9 oveq1d 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( ( abs ` ( x x. y ) ) ^ 2 ) = ( ( ( abs ` x ) x. ( abs ` y ) ) ^ 2 ) )
11 6 abscld 
 |-  ( x e. Z[i] -> ( abs ` x ) e. RR )
12 11 recnd 
 |-  ( x e. Z[i] -> ( abs ` x ) e. CC )
13 7 abscld 
 |-  ( y e. Z[i] -> ( abs ` y ) e. RR )
14 13 recnd 
 |-  ( y e. Z[i] -> ( abs ` y ) e. CC )
15 sqmul 
 |-  ( ( ( abs ` x ) e. CC /\ ( abs ` y ) e. CC ) -> ( ( ( abs ` x ) x. ( abs ` y ) ) ^ 2 ) = ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) )
16 12 14 15 syl2an 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( ( ( abs ` x ) x. ( abs ` y ) ) ^ 2 ) = ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) )
17 10 16 eqtr2d 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) = ( ( abs ` ( x x. y ) ) ^ 2 ) )
18 fveq2 
 |-  ( z = ( x x. y ) -> ( abs ` z ) = ( abs ` ( x x. y ) ) )
19 18 oveq1d 
 |-  ( z = ( x x. y ) -> ( ( abs ` z ) ^ 2 ) = ( ( abs ` ( x x. y ) ) ^ 2 ) )
20 19 rspceeqv 
 |-  ( ( ( x x. y ) e. Z[i] /\ ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) = ( ( abs ` ( x x. y ) ) ^ 2 ) ) -> E. z e. Z[i] ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) = ( ( abs ` z ) ^ 2 ) )
21 5 17 20 syl2anc 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> E. z e. Z[i] ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) = ( ( abs ` z ) ^ 2 ) )
22 1 2sqlem1 
 |-  ( ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) e. S <-> E. z e. Z[i] ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) = ( ( abs ` z ) ^ 2 ) )
23 21 22 sylibr 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) e. S )
24 oveq12 
 |-  ( ( A = ( ( abs ` x ) ^ 2 ) /\ B = ( ( abs ` y ) ^ 2 ) ) -> ( A x. B ) = ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) )
25 24 eleq1d 
 |-  ( ( A = ( ( abs ` x ) ^ 2 ) /\ B = ( ( abs ` y ) ^ 2 ) ) -> ( ( A x. B ) e. S <-> ( ( ( abs ` x ) ^ 2 ) x. ( ( abs ` y ) ^ 2 ) ) e. S ) )
26 23 25 syl5ibrcom 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( ( A = ( ( abs ` x ) ^ 2 ) /\ B = ( ( abs ` y ) ^ 2 ) ) -> ( A x. B ) e. S ) )
27 26 rexlimivv 
 |-  ( E. x e. Z[i] E. y e. Z[i] ( A = ( ( abs ` x ) ^ 2 ) /\ B = ( ( abs ` y ) ^ 2 ) ) -> ( A x. B ) e. S )
28 4 27 sylbir 
 |-  ( ( E. x e. Z[i] A = ( ( abs ` x ) ^ 2 ) /\ E. y e. Z[i] B = ( ( abs ` y ) ^ 2 ) ) -> ( A x. B ) e. S )
29 2 3 28 syl2anb 
 |-  ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )