This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrdi 
 |-  ( 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 ) ) )