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