Theorem imre

Description: The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005) (Revised by Mario Carneiro, 6-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		imval	|- ( A e. CC -> ( Im ` A ) = ( Re ` ( A / _i ) ) )
2		ax-icn	|- _i e. CC
3		ine0	|- _i =/= 0
4		divrec2	|- ( ( A e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( A / _i ) = ( ( 1 / _i ) x. A ) )
5	2 3 4	mp3an23	|- ( A e. CC -> ( A / _i ) = ( ( 1 / _i ) x. A ) )
6		irec	|- ( 1 / _i ) = -u _i
7	6	oveq1i	|- ( ( 1 / _i ) x. A ) = ( -u _i x. A )
8	5 7	syl6eq	|- ( A e. CC -> ( A / _i ) = ( -u _i x. A ) )
9	8	fveq2d	|- ( A e. CC -> ( Re ` ( A / _i ) ) = ( Re ` ( -u _i x. A ) ) )
10	1 9	eqtrd	|- ( A e. CC -> ( Im ` A ) = ( Re ` ( -u _i x. A ) ) )