Theorem cjmulrcl

Description: A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	cjmulrcl	$$⊢A\in ℂ\to A\bar{A}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		cjcj	$$⊢A\in ℂ\to \overline{\stackrel{‾}{A}}=A$$
2	1	oveq2d	$$⊢A\in ℂ\to \bar{A}\overline{\stackrel{‾}{A}}=\bar{A}A$$
3		cjcl	$$⊢A\in ℂ\to \bar{A}\in ℂ$$
4		cjmul	$$⊢\left(A\in ℂ\wedge \bar{A}\in ℂ\right)\to \overline{A\stackrel{‾}{A}}=\bar{A}\overline{\stackrel{‾}{A}}$$
5	3 4	mpdan	$$⊢A\in ℂ\to \overline{A\stackrel{‾}{A}}=\bar{A}\overline{\stackrel{‾}{A}}$$
6		mulcom	$$⊢\left(A\in ℂ\wedge \bar{A}\in ℂ\right)\to A\bar{A}=\bar{A}A$$
7	3 6	mpdan	$$⊢A\in ℂ\to A\bar{A}=\bar{A}A$$
8	2 5 7	3eqtr4d	$$⊢A\in ℂ\to \overline{A\stackrel{‾}{A}}=A\bar{A}$$
9		mulcl	$$⊢\left(A\in ℂ\wedge \bar{A}\in ℂ\right)\to A\bar{A}\in ℂ$$
10	3 9	mpdan	$$⊢A\in ℂ\to A\bar{A}\in ℂ$$
11		cjreb	$$⊢A\bar{A}\in ℂ\to \left(A\bar{A}\in ℝ\leftrightarrow \overline{A\stackrel{‾}{A}}=A\bar{A}\right)$$
12	10 11	syl	$$⊢A\in ℂ\to \left(A\bar{A}\in ℝ\leftrightarrow \overline{A\stackrel{‾}{A}}=A\bar{A}\right)$$
13	8 12	mpbird	$$⊢A\in ℂ\to A\bar{A}\in ℝ$$