absreimsq

Description: Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007)

		Ref	Expression
	Assertion	absreimsq	$⊢ (A \in ℝ \land B \in ℝ) \to {\|A + i B\|}^{2} = A^{2} + B^{2}$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		ax-icn	$⊢ i \in ℂ$
3		recn	$⊢ B \in ℝ \to B \in ℂ$
4		mulcl	$⊢ (i \in ℂ \land B \in ℂ) \to i B \in ℂ$
5	2 3 4	sylancr	$⊢ B \in ℝ \to i B \in ℂ$
6		addcl	$⊢ (A \in ℂ \land i B \in ℂ) \to A + i B \in ℂ$
7	1 5 6	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A + i B \in ℂ$
8		absvalsq2	$⊢ A + i B \in ℂ \to {\|A + i B\|}^{2} = {ℜ (A + i B)}^{2} + {ℑ (A + i B)}^{2}$
9	7 8	syl	$⊢ (A \in ℝ \land B \in ℝ) \to {\|A + i B\|}^{2} = {ℜ (A + i B)}^{2} + {ℑ (A + i B)}^{2}$
10		crre	$⊢ (A \in ℝ \land B \in ℝ) \to ℜ (A + i B) = A$
11	10	oveq1d	$⊢ (A \in ℝ \land B \in ℝ) \to {ℜ (A + i B)}^{2} = A^{2}$
12		crim	$⊢ (A \in ℝ \land B \in ℝ) \to ℑ (A + i B) = B$
13	12	oveq1d	$⊢ (A \in ℝ \land B \in ℝ) \to {ℑ (A + i B)}^{2} = B^{2}$
14	11 13	oveq12d	$⊢ (A \in ℝ \land B \in ℝ) \to {ℜ (A + i B)}^{2} + {ℑ (A + i B)}^{2} = A^{2} + B^{2}$
15	9 14	eqtrd	$⊢ (A \in ℝ \land B \in ℝ) \to {\|A + i B\|}^{2} = A^{2} + B^{2}$

Metamath Proof Explorer