Theorem ref

Description: Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007) (Revised by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	ref	|- Re : CC --> RR

Proof

Step	Hyp	Ref	Expression
1		df-re	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
2		reval	|- ( x e. CC -> ( Re ` x ) = ( ( x + ( * ` x ) ) / 2 ) )
3		recl	|- ( x e. CC -> ( Re ` x ) e. RR )
4	2 3	eqeltrrd	|- ( x e. CC -> ( ( x + ( * ` x ) ) / 2 ) e. RR )
5	1 4	fmpti	|- Re : CC --> RR