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