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	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		cjcj	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) = 𝐴 )
2	1	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐴 ) · 𝐴 ) )
3		cjcl	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
4		cjmul	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ) )
5	3 4	mpdan	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ) )
6		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) = ( ( ∗ ‘ 𝐴 ) · 𝐴 ) )
7	3 6	mpdan	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) = ( ( ∗ ‘ 𝐴 ) · 𝐴 ) )
8	2 5 7	3eqtr4d	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
9		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
10	3 9	mpdan	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
11		cjreb	⊢ ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℂ → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ↔ ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
12	10 11	syl	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ↔ ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
13	8 12	mpbird	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ )