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 ) ) )