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 · ( ℜ ‘ 𝐴 ) ) )