Metamath Proof Explorer

Theorem bhmafibid2

Description: The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020)

Ref Expression
Assertion bhmafibid2 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR )
2 1 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. CC )
3 2 sqcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C ^ 2 ) e. CC )
4 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR )
5 4 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. CC )
6 5 sqcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( D ^ 2 ) e. CC )
7 3 6 addcomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( C ^ 2 ) + ( D ^ 2 ) ) = ( ( D ^ 2 ) + ( C ^ 2 ) ) )
8 7 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( D ^ 2 ) + ( C ^ 2 ) ) ) )
9 bhmafibid1 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( D e. RR /\ C e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( D ^ 2 ) + ( C ^ 2 ) ) ) = ( ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) + ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) ) )
10 9 ancom2s 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( D ^ 2 ) + ( C ^ 2 ) ) ) = ( ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) + ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) ) )
11 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. RR )
12 11 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. CC )
13 12 5 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A x. D ) e. CC )
14 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. RR )
15 14 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. CC )
16 15 2 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. C ) e. CC )
17 13 16 subcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A x. D ) - ( B x. C ) ) e. CC )
18 17 sqcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) e. CC )
19 12 2 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A x. C ) e. CC )
20 15 5 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. D ) e. CC )
21 19 20 addcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A x. C ) + ( B x. D ) ) e. CC )
22 21 sqcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) e. CC )
23 18 22 addcomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) + ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) ) = ( ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) ) )
24 8 10 23 3eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) ) )