Theorem 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\bar{A}={\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$

Proof

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