Step |
Hyp |
Ref |
Expression |
1 |
|
cjsub |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 − 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) ) |
2 |
1
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) · ( ∗ ‘ ( 𝐴 − 𝐵 ) ) ) = ( ( 𝐴 − 𝐵 ) · ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) ) ) |
3 |
|
cjcl |
⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ ) |
4 |
|
cjcl |
⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) ∈ ℂ ) |
5 |
3 4
|
anim12i |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) ) |
6 |
|
mulsub |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) · ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) − ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) ) |
7 |
5 6
|
mpdan |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) · ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐵 ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) − ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) ) |
8 |
2 7
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) · ( ∗ ‘ ( 𝐴 − 𝐵 ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) − ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) ) |
9 |
|
subcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ ) |
10 |
|
absvalsq |
⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) · ( ∗ ‘ ( 𝐴 − 𝐵 ) ) ) ) |
11 |
9 10
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) · ( ∗ ‘ ( 𝐴 − 𝐵 ) ) ) ) |
12 |
|
absvalsq |
⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) |
13 |
|
absvalsq |
⊢ ( 𝐵 ∈ ℂ → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) |
14 |
|
mulcom |
⊢ ( ( 𝐵 ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) → ( 𝐵 · ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) |
15 |
4 14
|
mpdan |
⊢ ( 𝐵 ∈ ℂ → ( 𝐵 · ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) |
16 |
13 15
|
eqtrd |
⊢ ( 𝐵 ∈ ℂ → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) |
17 |
12 16
|
oveqan12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) ) |
18 |
|
mulcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) → ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ∈ ℂ ) |
19 |
4 18
|
sylan2 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ∈ ℂ ) |
20 |
19
|
addcjd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) = ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) |
21 |
|
cjmul |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) ) ) |
22 |
4 21
|
sylan2 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) ) ) |
23 |
|
cjcj |
⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) = 𝐵 ) |
24 |
23
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) = 𝐵 ) |
25 |
24
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) |
26 |
22 25
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) |
27 |
26
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) |
28 |
20 27
|
eqtr3d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) |
29 |
17 28
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) − ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) ) |
30 |
8 11 29
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) ) |