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

Metamath Proof Explorer

Theorem imval2

Description: The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion imval2 
|- ( A e. CC -> ( Im ` A ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )

Proof

Step Hyp Ref Expression
1 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
2 1 recnd 
 |-  ( A e. CC -> ( Im ` A ) e. CC )
3 2mulicn 
 |-  ( 2 x. _i ) e. CC
4 2muline0 
 |-  ( 2 x. _i ) =/= 0
5 divcan4 
 |-  ( ( ( Im ` A ) e. CC /\ ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> ( ( ( Im ` A ) x. ( 2 x. _i ) ) / ( 2 x. _i ) ) = ( Im ` A ) )
6 3 4 5 mp3an23 
 |-  ( ( Im ` A ) e. CC -> ( ( ( Im ` A ) x. ( 2 x. _i ) ) / ( 2 x. _i ) ) = ( Im ` A ) )
7 2 6 syl 
 |-  ( A e. CC -> ( ( ( Im ` A ) x. ( 2 x. _i ) ) / ( 2 x. _i ) ) = ( Im ` A ) )
8 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
9 8 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
10 ax-icn 
 |-  _i e. CC
11 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
12 10 2 11 sylancr 
 |-  ( A e. CC -> ( _i x. ( Im ` A ) ) e. CC )
13 9 12 addcld 
 |-  ( A e. CC -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) e. CC )
14 13 9 12 subsubd 
 |-  ( A e. CC -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) = ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( Re ` A ) ) + ( _i x. ( Im ` A ) ) ) )
15 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
16 remim 
 |-  ( A e. CC -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
17 15 16 oveq12d 
 |-  ( A e. CC -> ( A - ( * ` A ) ) = ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) )
18 12 2timesd 
 |-  ( A e. CC -> ( 2 x. ( _i x. ( Im ` A ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` A ) ) ) )
19 mulcom 
 |-  ( ( ( Im ` A ) e. CC /\ ( 2 x. _i ) e. CC ) -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( ( 2 x. _i ) x. ( Im ` A ) ) )
20 3 19 mpan2 
 |-  ( ( Im ` A ) e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( ( 2 x. _i ) x. ( Im ` A ) ) )
21 2cn 
 |-  2 e. CC
22 mulass 
 |-  ( ( 2 e. CC /\ _i e. CC /\ ( Im ` A ) e. CC ) -> ( ( 2 x. _i ) x. ( Im ` A ) ) = ( 2 x. ( _i x. ( Im ` A ) ) ) )
23 21 10 22 mp3an12 
 |-  ( ( Im ` A ) e. CC -> ( ( 2 x. _i ) x. ( Im ` A ) ) = ( 2 x. ( _i x. ( Im ` A ) ) ) )
24 20 23 eqtrd 
 |-  ( ( Im ` A ) e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( 2 x. ( _i x. ( Im ` A ) ) ) )
25 2 24 syl 
 |-  ( A e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( 2 x. ( _i x. ( Im ` A ) ) ) )
26 9 12 pncan2d 
 |-  ( A e. CC -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( Re ` A ) ) = ( _i x. ( Im ` A ) ) )
27 26 oveq1d 
 |-  ( A e. CC -> ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( Re ` A ) ) + ( _i x. ( Im ` A ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` A ) ) ) )
28 18 25 27 3eqtr4d 
 |-  ( A e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( Re ` A ) ) + ( _i x. ( Im ` A ) ) ) )
29 14 17 28 3eqtr4rd 
 |-  ( A e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( A - ( * ` A ) ) )
30 29 oveq1d 
 |-  ( A e. CC -> ( ( ( Im ` A ) x. ( 2 x. _i ) ) / ( 2 x. _i ) ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )
31 7 30 eqtr3d 
 |-  ( A e. CC -> ( Im ` A ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )