Metamath Proof Explorer


Theorem sqabssub

Description: Square of absolute value of difference. (Contributed by NM, 21-Jan-2007)

Ref Expression
Assertion sqabssub
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cjsub
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A - B ) ) = ( ( * ` A ) - ( * ` B ) ) )
2 1 oveq2d
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) x. ( * ` ( A - B ) ) ) = ( ( A - B ) x. ( ( * ` A ) - ( * ` B ) ) ) )
3 cjcl
 |-  ( A e. CC -> ( * ` A ) e. CC )
4 cjcl
 |-  ( B e. CC -> ( * ` B ) e. CC )
5 3 4 anim12i
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) e. CC /\ ( * ` B ) e. CC ) )
6 mulsub
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( * ` A ) e. CC /\ ( * ` B ) e. CC ) ) -> ( ( A - B ) x. ( ( * ` A ) - ( * ` B ) ) ) = ( ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) - ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) ) )
7 5 6 mpdan
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) x. ( ( * ` A ) - ( * ` B ) ) ) = ( ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) - ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) ) )
8 2 7 eqtrd
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) x. ( * ` ( A - B ) ) ) = ( ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) - ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) ) )
9 subcl
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
10 absvalsq
 |-  ( ( A - B ) e. CC -> ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( A - B ) x. ( * ` ( A - B ) ) ) )
11 9 10 syl
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( A - B ) x. ( * ` ( A - B ) ) ) )
12 absvalsq
 |-  ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
13 absvalsq
 |-  ( B e. CC -> ( ( abs ` B ) ^ 2 ) = ( B x. ( * ` B ) ) )
14 mulcom
 |-  ( ( B e. CC /\ ( * ` B ) e. CC ) -> ( B x. ( * ` B ) ) = ( ( * ` B ) x. B ) )
15 4 14 mpdan
 |-  ( B e. CC -> ( B x. ( * ` B ) ) = ( ( * ` B ) x. B ) )
16 13 15 eqtrd
 |-  ( B e. CC -> ( ( abs ` B ) ^ 2 ) = ( ( * ` B ) x. B ) )
17 12 16 oveqan12d
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) = ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) )
18 mulcl
 |-  ( ( A e. CC /\ ( * ` B ) e. CC ) -> ( A x. ( * ` B ) ) e. CC )
19 4 18 sylan2
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. ( * ` B ) ) e. CC )
20 19 addcjd
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. ( * ` B ) ) + ( * ` ( A x. ( * ` B ) ) ) ) = ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) )
21 cjmul
 |-  ( ( A e. CC /\ ( * ` B ) e. CC ) -> ( * ` ( A x. ( * ` B ) ) ) = ( ( * ` A ) x. ( * ` ( * ` B ) ) ) )
22 4 21 sylan2
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. ( * ` B ) ) ) = ( ( * ` A ) x. ( * ` ( * ` B ) ) ) )
23 cjcj
 |-  ( B e. CC -> ( * ` ( * ` B ) ) = B )
24 23 adantl
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( * ` B ) ) = B )
25 24 oveq2d
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) x. ( * ` ( * ` B ) ) ) = ( ( * ` A ) x. B ) )
26 22 25 eqtrd
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. ( * ` B ) ) ) = ( ( * ` A ) x. B ) )
27 26 oveq2d
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. ( * ` B ) ) + ( * ` ( A x. ( * ` B ) ) ) ) = ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) )
28 20 27 eqtr3d
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) = ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) )
29 17 28 oveq12d
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) = ( ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) - ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) ) )
30 8 11 29 3eqtr4d
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )