Theorem reval

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

	Ref	Expression
Assertion	reval	|- ( A e. CC -> ( Re ` A ) = ( ( A + ( * ` A ) ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( x = A -> ( * ` x ) = ( * ` A ) )
2		oveq12	|- ( ( x = A /\ ( * ` x ) = ( * ` A ) ) -> ( x + ( * ` x ) ) = ( A + ( * ` A ) ) )
3	1 2	mpdan	|- ( x = A -> ( x + ( * ` x ) ) = ( A + ( * ` A ) ) )
4	3	oveq1d	|- ( x = A -> ( ( x + ( * ` x ) ) / 2 ) = ( ( A + ( * ` A ) ) / 2 ) )
5		df-re	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
6		ovex	|- ( ( A + ( * ` A ) ) / 2 ) e. _V
7	4 5 6	fvmpt	|- ( A e. CC -> ( Re ` A ) = ( ( A + ( * ` A ) ) / 2 ) )