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

Metamath Proof Explorer

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