Metamath Proof Explorer

Theorem bhmafibid1cn

Description: The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. First result. (Contributed by Thierry Arnoux, 1-Feb-2020) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023)

Ref Expression
Assertion bhmafibid1cn 
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( 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 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> A e. CC )
2 1 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A ^ 2 ) e. CC )
3 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> C e. CC )
4 3 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( C ^ 2 ) e. CC )
5 2 4 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A ^ 2 ) x. ( C ^ 2 ) ) e. CC )
6 simprr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> D e. CC )
7 6 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( D ^ 2 ) e. CC )
8 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> B e. CC )
9 8 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B ^ 2 ) e. CC )
10 7 9 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( D ^ 2 ) x. ( B ^ 2 ) ) e. CC )
11 2 7 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A ^ 2 ) x. ( D ^ 2 ) ) e. CC )
12 4 9 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( C ^ 2 ) x. ( B ^ 2 ) ) e. CC )
13 5 10 11 12 add4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) + ( ( ( A ^ 2 ) x. ( D ^ 2 ) ) + ( ( C ^ 2 ) x. ( B ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( D ^ 2 ) ) ) + ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( ( C ^ 2 ) x. ( B ^ 2 ) ) ) ) )
14 7 9 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( D ^ 2 ) x. ( B ^ 2 ) ) = ( ( B ^ 2 ) x. ( D ^ 2 ) ) )
15 4 9 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( C ^ 2 ) x. ( B ^ 2 ) ) = ( ( B ^ 2 ) x. ( C ^ 2 ) ) )
16 14 15 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( ( C ^ 2 ) x. ( B ^ 2 ) ) ) = ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
17 16 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( D ^ 2 ) ) ) + ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( ( C ^ 2 ) x. ( B ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( D ^ 2 ) ) ) + ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) ) )
18 13 17 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) + ( ( ( A ^ 2 ) x. ( D ^ 2 ) ) + ( ( C ^ 2 ) x. ( B ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( D ^ 2 ) ) ) + ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) ) )
19 2 9 4 7 muladdd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) + ( ( ( A ^ 2 ) x. ( D ^ 2 ) ) + ( ( C ^ 2 ) x. ( B ^ 2 ) ) ) ) )
20 1 3 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A x. C ) e. CC )
21 8 6 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. D ) e. CC )
22 binom2sub 
 |-  ( ( ( A x. C ) e. CC /\ ( B x. D ) e. CC ) -> ( ( ( A x. C ) - ( B x. D ) ) ^ 2 ) = ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( B x. D ) ^ 2 ) ) )
23 20 21 22 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) - ( B x. D ) ) ^ 2 ) = ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( B x. D ) ^ 2 ) ) )
24 1 6 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A x. D ) e. CC )
25 8 3 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. C ) e. CC )
26 binom2 
 |-  ( ( ( A x. D ) e. CC /\ ( B x. C ) e. CC ) -> ( ( ( A x. D ) + ( B x. C ) ) ^ 2 ) = ( ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) + ( ( B x. C ) ^ 2 ) ) )
27 24 25 26 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. D ) + ( B x. C ) ) ^ 2 ) = ( ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) + ( ( B x. C ) ^ 2 ) ) )
28 23 27 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A x. C ) - ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) + ( B x. C ) ) ^ 2 ) ) = ( ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( B x. D ) ^ 2 ) ) + ( ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) + ( ( B x. C ) ^ 2 ) ) ) )
29 20 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. C ) ^ 2 ) e. CC )
30 2cnd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> 2 e. CC )
31 20 21 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. C ) x. ( B x. D ) ) e. CC )
32 30 31 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) e. CC )
33 29 32 subcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) e. CC )
34 21 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( B x. D ) ^ 2 ) e. CC )
35 24 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. D ) ^ 2 ) e. CC )
36 24 25 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. D ) x. ( B x. C ) ) e. CC )
37 30 36 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) e. CC )
38 35 37 addcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) e. CC )
39 25 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( B x. C ) ^ 2 ) e. CC )
40 33 34 38 39 add4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( B x. D ) ^ 2 ) ) + ( ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) + ( ( B x. C ) ^ 2 ) ) ) = ( ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) ) + ( ( ( B x. D ) ^ 2 ) + ( ( B x. C ) ^ 2 ) ) ) )
41 mul4r 
 |-  ( ( ( A e. CC /\ C e. CC ) /\ ( B e. CC /\ D e. CC ) ) -> ( ( A x. C ) x. ( B x. D ) ) = ( ( A x. D ) x. ( B x. C ) ) )
42 41 an4s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. C ) x. ( B x. D ) ) = ( ( A x. D ) x. ( B x. C ) ) )
43 42 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) = ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) )
44 43 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) = ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) )
45 44 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) ) = ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) + ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) ) )
46 29 37 35 nppcan3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) + ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) ) = ( ( ( A x. C ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) )
47 45 46 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) ) = ( ( ( A x. C ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) )
48 8 6 sqmuld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( B x. D ) ^ 2 ) = ( ( B ^ 2 ) x. ( D ^ 2 ) ) )
49 8 3 sqmuld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( B x. C ) ^ 2 ) = ( ( B ^ 2 ) x. ( C ^ 2 ) ) )
50 48 49 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( B x. D ) ^ 2 ) + ( ( B x. C ) ^ 2 ) ) = ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
51 47 50 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) ) + ( ( ( B x. D ) ^ 2 ) + ( ( B x. C ) ^ 2 ) ) ) = ( ( ( ( A x. C ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) + ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) ) )
52 1 3 sqmuld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. C ) ^ 2 ) = ( ( A ^ 2 ) x. ( C ^ 2 ) ) )
53 1 6 sqmuld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. D ) ^ 2 ) = ( ( A ^ 2 ) x. ( D ^ 2 ) ) )
54 52 53 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) = ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( D ^ 2 ) ) ) )
55 54 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A x. C ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) + ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( D ^ 2 ) ) ) + ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) ) )
56 51 55 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. D ) ) ) ) + ( ( ( A x. D ) ^ 2 ) + ( 2 x. ( ( A x. D ) x. ( B x. C ) ) ) ) ) + ( ( ( B x. D ) ^ 2 ) + ( ( B x. C ) ^ 2 ) ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( D ^ 2 ) ) ) + ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) ) )
57 28 40 56 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A x. C ) - ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) + ( B x. C ) ) ^ 2 ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( D ^ 2 ) ) ) + ( ( ( B ^ 2 ) x. ( D ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) ) )
58 18 19 57 3eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( ( A x. C ) - ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) + ( B x. C ) ) ^ 2 ) ) )