cjmulval

Description: A complex number times its conjugate. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 14-Jul-2014)

		Ref	Expression
	Assertion	cjmulval	$⊢ A \in ℂ \to A \overline{A} = {ℜ (A)}^{2} + {ℑ (A)}^{2}$

Step	Hyp	Ref	Expression
1		recl	$⊢ A \in ℂ \to ℜ (A) \in ℝ$
2	1	recnd	$⊢ A \in ℂ \to ℜ (A) \in ℂ$
3	2	sqvald	$⊢ A \in ℂ \to {ℜ (A)}^{2} = ℜ (A) ℜ (A)$
4		imcl	$⊢ A \in ℂ \to ℑ (A) \in ℝ$
5	4	recnd	$⊢ A \in ℂ \to ℑ (A) \in ℂ$
6	5	sqvald	$⊢ A \in ℂ \to {ℑ (A)}^{2} = ℑ (A) ℑ (A)$
7	3 6	oveq12d	$⊢ A \in ℂ \to {ℜ (A)}^{2} + {ℑ (A)}^{2} = ℜ (A) ℜ (A) + ℑ (A) ℑ (A)$
8		ipcnval	$⊢ (A \in ℂ \land A \in ℂ) \to ℜ (A \overline{A}) = ℜ (A) ℜ (A) + ℑ (A) ℑ (A)$
9	8	anidms	$⊢ A \in ℂ \to ℜ (A \overline{A}) = ℜ (A) ℜ (A) + ℑ (A) ℑ (A)$
10		cjmulrcl	$⊢ A \in ℂ \to A \overline{A} \in ℝ$
11		rere	$⊢ A \overline{A} \in ℝ \to ℜ (A \overline{A}) = A \overline{A}$
12	10 11	syl	$⊢ A \in ℂ \to ℜ (A \overline{A}) = A \overline{A}$
13	7 9 12	3eqtr2rd	$⊢ A \in ℂ \to A \overline{A} = {ℜ (A)}^{2} + {ℑ (A)}^{2}$

Metamath Proof Explorer