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