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 \overline{A} \in ℝ$

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

Metamath Proof Explorer