Metamath Proof Explorer

Theorem sqabssub

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

Ref Expression
Assertion sqabssub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) )

Proof

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 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) )