sqabssub

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

		Ref	Expression
	Assertion	sqabssub	$⊢ (A \in ℂ \land B \in ℂ) \to {\|A - B\|}^{2} = {\|A\|}^{2} + {\|B\|}^{2} - 2 ℜ (A \overline{B})$

Proof

Step	Hyp	Ref	Expression
1		cjsub	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A - B} = \overline{A} - \overline{B}$
2	1	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to (A - B) \overline{A - B} = (A - B) (\overline{A} - \overline{B})$
3		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
4		cjcl	$⊢ B \in ℂ \to \overline{B} \in ℂ$
5	3 4	anim12i	$⊢ (A \in ℂ \land B \in ℂ) \to (\overline{A} \in ℂ \land \overline{B} \in ℂ)$
6		mulsub	$⊢ ((A \in ℂ \land B \in ℂ) \land (\overline{A} \in ℂ \land \overline{B} \in ℂ)) \to (A - B) (\overline{A} - \overline{B}) = A \overline{A} + \overline{B} B - (A \overline{B} + \overline{A} B)$
7	5 6	mpdan	$⊢ (A \in ℂ \land B \in ℂ) \to (A - B) (\overline{A} - \overline{B}) = A \overline{A} + \overline{B} B - (A \overline{B} + \overline{A} B)$
8	2 7	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to (A - B) \overline{A - B} = A \overline{A} + \overline{B} B - (A \overline{B} + \overline{A} B)$
9		subcl	$⊢ (A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
10		absvalsq	$⊢ A - B \in ℂ \to {\|A - B\|}^{2} = (A - B) \overline{A - B}$
11	9 10	syl	$⊢ (A \in ℂ \land B \in ℂ) \to {\|A - B\|}^{2} = (A - B) \overline{A - B}$
12		absvalsq	$⊢ A \in ℂ \to {\|A\|}^{2} = A \overline{A}$
13		absvalsq	$⊢ B \in ℂ \to {\|B\|}^{2} = B \overline{B}$
14		mulcom	$⊢ (B \in ℂ \land \overline{B} \in ℂ) \to B \overline{B} = \overline{B} B$
15	4 14	mpdan	$⊢ B \in ℂ \to B \overline{B} = \overline{B} B$
16	13 15	eqtrd	$⊢ B \in ℂ \to {\|B\|}^{2} = \overline{B} B$
17	12 16	oveqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to {\|A\|}^{2} + {\|B\|}^{2} = A \overline{A} + \overline{B} B$
18		mulcl	$⊢ (A \in ℂ \land \overline{B} \in ℂ) \to A \overline{B} \in ℂ$
19	4 18	sylan2	$⊢ (A \in ℂ \land B \in ℂ) \to A \overline{B} \in ℂ$
20	19	addcjd	$⊢ (A \in ℂ \land B \in ℂ) \to A \overline{B} + \overline{A \overline{B}} = 2 ℜ (A \overline{B})$
21		cjmul	$⊢ (A \in ℂ \land \overline{B} \in ℂ) \to \overline{A \overline{B}} = \overline{A} \overline{\overline{B}}$
22	4 21	sylan2	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A \overline{B}} = \overline{A} \overline{\overline{B}}$
23		cjcj	$⊢ B \in ℂ \to \overline{\overline{B}} = B$
24	23	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{\overline{B}} = B$
25	24	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A} \overline{\overline{B}} = \overline{A} B$
26	22 25	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A \overline{B}} = \overline{A} B$
27	26	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to A \overline{B} + \overline{A \overline{B}} = A \overline{B} + \overline{A} B$
28	20 27	eqtr3d	$⊢ (A \in ℂ \land B \in ℂ) \to 2 ℜ (A \overline{B}) = A \overline{B} + \overline{A} B$
29	17 28	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to {\|A\|}^{2} + {\|B\|}^{2} - 2 ℜ (A \overline{B}) = A \overline{A} + \overline{B} B - (A \overline{B} + \overline{A} B)$
30	8 11 29	3eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to {\|A - B\|}^{2} = {\|A\|}^{2} + {\|B\|}^{2} - 2 ℜ (A \overline{B})$

Metamath Proof Explorer

Theorem sqabssub

Proof