Theorem sqabssub

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

	Ref	Expression
Assertion	sqabssub	|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )

Proof

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