Metamath Proof Explorer


Theorem sqabssubi

Description: Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007)

Ref Expression
Hypotheses absvalsqi.1
|- A e. CC
abssub.2
|- B e. CC
Assertion sqabssubi
|- ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 absvalsqi.1
 |-  A e. CC
2 abssub.2
 |-  B e. CC
3 sqabssub
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )
4 1 2 3 mp2an
 |-  ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) )