Metamath Proof Explorer

Theorem bhmafibid1

Description: The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. First result. Remark: The proof uses a different approach than the proof of bhmafibid1cn , and is a little bit shorter. (Contributed by Thierry Arnoux, 1-Feb-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bhmafibid1 
|- ( ( ( 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 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. RR )
2 1 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. CC )
3 ax-icn 
 |-  _i e. CC
4 3 a1i 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> _i e. CC )
5 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. RR )
6 5 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. CC )
7 4 6 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( _i x. B ) e. CC )
8 2 7 addcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A + ( _i x. B ) ) e. CC )
9 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR )
10 9 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. CC )
11 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR )
12 11 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. CC )
13 4 12 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( _i x. D ) e. CC )
14 10 13 addcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C + ( _i x. D ) ) e. CC )
15 8 14 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) e. CC )
16 15 replimd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) = ( ( Re ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) + ( _i x. ( Im ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) ) ) )
17 8 14 remuld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( Re ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) = ( ( ( Re ` ( A + ( _i x. B ) ) ) x. ( Re ` ( C + ( _i x. D ) ) ) ) - ( ( Im ` ( A + ( _i x. B ) ) ) x. ( Im ` ( C + ( _i x. D ) ) ) ) ) )
18 1 5 crred 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( Re ` ( A + ( _i x. B ) ) ) = A )
19 9 11 crred 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( Re ` ( C + ( _i x. D ) ) ) = C )
20 18 19 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( Re ` ( A + ( _i x. B ) ) ) x. ( Re ` ( C + ( _i x. D ) ) ) ) = ( A x. C ) )
21 1 5 crimd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( Im ` ( A + ( _i x. B ) ) ) = B )
22 9 11 crimd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( Im ` ( C + ( _i x. D ) ) ) = D )
23 21 22 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( Im ` ( A + ( _i x. B ) ) ) x. ( Im ` ( C + ( _i x. D ) ) ) ) = ( B x. D ) )
24 20 23 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( Re ` ( A + ( _i x. B ) ) ) x. ( Re ` ( C + ( _i x. D ) ) ) ) - ( ( Im ` ( A + ( _i x. B ) ) ) x. ( Im ` ( C + ( _i x. D ) ) ) ) ) = ( ( A x. C ) - ( B x. D ) ) )
25 17 24 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( Re ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) = ( ( A x. C ) - ( B x. D ) ) )
26 8 14 immuld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( Im ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) = ( ( ( Re ` ( A + ( _i x. B ) ) ) x. ( Im ` ( C + ( _i x. D ) ) ) ) + ( ( Im ` ( A + ( _i x. B ) ) ) x. ( Re ` ( C + ( _i x. D ) ) ) ) ) )
27 18 22 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( Re ` ( A + ( _i x. B ) ) ) x. ( Im ` ( C + ( _i x. D ) ) ) ) = ( A x. D ) )
28 21 19 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( Im ` ( A + ( _i x. B ) ) ) x. ( Re ` ( C + ( _i x. D ) ) ) ) = ( B x. C ) )
29 27 28 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( Re ` ( A + ( _i x. B ) ) ) x. ( Im ` ( C + ( _i x. D ) ) ) ) + ( ( Im ` ( A + ( _i x. B ) ) ) x. ( Re ` ( C + ( _i x. D ) ) ) ) ) = ( ( A x. D ) + ( B x. C ) ) )
30 26 29 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( Im ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) = ( ( A x. D ) + ( B x. C ) ) )
31 30 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( _i x. ( Im ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) ) = ( _i x. ( ( A x. D ) + ( B x. C ) ) ) )
32 25 31 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( Re ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) + ( _i x. ( Im ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) ) ) = ( ( ( A x. C ) - ( B x. D ) ) + ( _i x. ( ( A x. D ) + ( B x. C ) ) ) ) )
33 16 32 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) = ( ( ( A x. C ) - ( B x. D ) ) + ( _i x. ( ( A x. D ) + ( B x. C ) ) ) ) )
34 33 fveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( abs ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) = ( abs ` ( ( ( A x. C ) - ( B x. D ) ) + ( _i x. ( ( A x. D ) + ( B x. C ) ) ) ) ) )
35 34 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( abs ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) ^ 2 ) = ( ( abs ` ( ( ( A x. C ) - ( B x. D ) ) + ( _i x. ( ( A x. D ) + ( B x. C ) ) ) ) ) ^ 2 ) )
36 8 14 absmuld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( abs ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) = ( ( abs ` ( A + ( _i x. B ) ) ) x. ( abs ` ( C + ( _i x. D ) ) ) ) )
37 36 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( abs ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) ^ 2 ) = ( ( ( abs ` ( A + ( _i x. B ) ) ) x. ( abs ` ( C + ( _i x. D ) ) ) ) ^ 2 ) )
38 8 abscld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( abs ` ( A + ( _i x. B ) ) ) e. RR )
39 38 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( abs ` ( A + ( _i x. B ) ) ) e. CC )
40 14 abscld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( abs ` ( C + ( _i x. D ) ) ) e. RR )
41 40 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( abs ` ( C + ( _i x. D ) ) ) e. CC )
42 39 41 sqmuld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( abs ` ( A + ( _i x. B ) ) ) x. ( abs ` ( C + ( _i x. D ) ) ) ) ^ 2 ) = ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) x. ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) )
43 absreimsq 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
44 absreimsq 
 |-  ( ( C e. RR /\ D e. RR ) -> ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
45 43 44 oveqan12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) x. ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
46 37 42 45 3eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( abs ` ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) ) ^ 2 ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
47 1 9 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A x. C ) e. RR )
48 5 11 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. D ) e. RR )
49 47 48 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A x. C ) - ( B x. D ) ) e. RR )
50 1 11 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A x. D ) e. RR )
51 5 9 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. C ) e. RR )
52 50 51 readdcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A x. D ) + ( B x. C ) ) e. RR )
53 absreimsq 
 |-  ( ( ( ( A x. C ) - ( B x. D ) ) e. RR /\ ( ( A x. D ) + ( B x. C ) ) e. RR ) -> ( ( abs ` ( ( ( A x. C ) - ( B x. D ) ) + ( _i x. ( ( A x. D ) + ( B x. C ) ) ) ) ) ^ 2 ) = ( ( ( ( A x. C ) - ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) + ( B x. C ) ) ^ 2 ) ) )
54 49 52 53 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( abs ` ( ( ( A x. C ) - ( B x. D ) ) + ( _i x. ( ( A x. D ) + ( B x. C ) ) ) ) ) ^ 2 ) = ( ( ( ( A x. C ) - ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) + ( B x. C ) ) ^ 2 ) ) )
55 35 46 54 3eqtr3d 
 |-  ( ( ( 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 ) ) )