This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addcj

Description: A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of Gleason p. 133. (Contributed by NM, 21-Jan-2007) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion addcj ( 𝐴 ∈ ℂ → ( 𝐴 + ( ∗ ‘ 𝐴 ) ) = ( 2 · ( ℜ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 reval ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) )
2 1 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( ℜ ‘ 𝐴 ) ) = ( 2 · ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) ) )
3 cjcl ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
4 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
5 3 4 mpdan ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
6 2cn ⊢ 2 ∈ ℂ
7 2ne0 ⊢ 2 ≠ 0
8 divcan2 ⊢ ( ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) ) = ( 𝐴 + ( ∗ ‘ 𝐴 ) ) )
9 6 7 8 mp3an23 ⊢ ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℂ → ( 2 · ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) ) = ( 𝐴 + ( ∗ ‘ 𝐴 ) ) )
10 5 9 syl ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) ) = ( 𝐴 + ( ∗ ‘ 𝐴 ) ) )
11 2 10 eqtr2d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ∗ ‘ 𝐴 ) ) = ( 2 · ( ℜ ‘ 𝐴 ) ) )