Theorem reim

Description: The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	reim	|- ( A e. CC -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	|- _i e. CC
2		mulcl	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
3	1 2	mpan	|- ( A e. CC -> ( _i x. A ) e. CC )
4		imval	|- ( ( _i x. A ) e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` ( ( _i x. A ) / _i ) ) )
5	3 4	syl	|- ( A e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` ( ( _i x. A ) / _i ) ) )
6		ine0	|- _i =/= 0
7		divcan3	|- ( ( A e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( _i x. A ) / _i ) = A )
8	1 6 7	mp3an23	|- ( A e. CC -> ( ( _i x. A ) / _i ) = A )
9	8	fveq2d	|- ( A e. CC -> ( Re ` ( ( _i x. A ) / _i ) ) = ( Re ` A ) )
10	5 9	eqtr2d	|- ( A e. CC -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )