Theorem recl

Description: The real part of a complex number is real. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	recl	|- ( A e. CC -> ( Re ` A ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		reval	|- ( A e. CC -> ( Re ` A ) = ( ( A + ( * ` A ) ) / 2 ) )
2		cjth	|- ( A e. CC -> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) )
3	2	simpld	|- ( A e. CC -> ( A + ( * ` A ) ) e. RR )
4	3	rehalfcld	|- ( A e. CC -> ( ( A + ( * ` A ) ) / 2 ) e. RR )
5	1 4	eqeltrd	|- ( A e. CC -> ( Re ` A ) e. RR )