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 
|- ( A e. CC -> ( A + ( * ` A ) ) = ( 2 x. ( Re ` A ) ) )

Proof

Step Hyp Ref Expression
1 reval 
 |-  ( A e. CC -> ( Re ` A ) = ( ( A + ( * ` A ) ) / 2 ) )
2 1 oveq2d 
 |-  ( A e. CC -> ( 2 x. ( Re ` A ) ) = ( 2 x. ( ( A + ( * ` A ) ) / 2 ) ) )
3 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
4 addcl 
 |-  ( ( A e. CC /\ ( * ` A ) e. CC ) -> ( A + ( * ` A ) ) e. CC )
5 3 4 mpdan 
 |-  ( A e. CC -> ( A + ( * ` A ) ) e. CC )
6 2cn 
 |-  2 e. CC
7 2ne0 
 |-  2 =/= 0
8 divcan2 
 |-  ( ( ( A + ( * ` A ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( ( A + ( * ` A ) ) / 2 ) ) = ( A + ( * ` A ) ) )
9 6 7 8 mp3an23 
 |-  ( ( A + ( * ` A ) ) e. CC -> ( 2 x. ( ( A + ( * ` A ) ) / 2 ) ) = ( A + ( * ` A ) ) )
10 5 9 syl 
 |-  ( A e. CC -> ( 2 x. ( ( A + ( * ` A ) ) / 2 ) ) = ( A + ( * ` A ) ) )
11 2 10 eqtr2d 
 |-  ( A e. CC -> ( A + ( * ` A ) ) = ( 2 x. ( Re ` A ) ) )