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 ) ) ) ) ) ) |