Metamath Proof Explorer


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