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

Metamath Proof Explorer

Theorem efiarg

Description: The exponential of the "arg" function Im o. log . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion efiarg 
|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )

Proof

Step Hyp Ref Expression
1 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
2 1 recld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) e. RR )
3 2 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) e. CC )
4 efsub 
 |-  ( ( ( log ` A ) e. CC /\ ( Re ` ( log ` A ) ) e. CC ) -> ( exp ` ( ( log ` A ) - ( Re ` ( log ` A ) ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( Re ` ( log ` A ) ) ) ) )
5 1 3 4 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( ( log ` A ) - ( Re ` ( log ` A ) ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( Re ` ( log ` A ) ) ) ) )
6 ax-icn 
 |-  _i e. CC
7 1 imcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. RR )
8 7 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. CC )
9 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` ( log ` A ) ) e. CC ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
10 6 8 9 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
11 1 replimd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) = ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) )
12 3 10 11 mvrladdd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( log ` A ) - ( Re ` ( log ` A ) ) ) = ( _i x. ( Im ` ( log ` A ) ) ) )
13 12 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( ( log ` A ) - ( Re ` ( log ` A ) ) ) ) = ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) )
14 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
15 relog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) = ( log ` ( abs ` A ) ) )
16 15 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( Re ` ( log ` A ) ) ) = ( exp ` ( log ` ( abs ` A ) ) ) )
17 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
18 17 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR )
19 18 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. CC )
20 absrpcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
21 20 rpne0d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) =/= 0 )
22 eflog 
 |-  ( ( ( abs ` A ) e. CC /\ ( abs ` A ) =/= 0 ) -> ( exp ` ( log ` ( abs ` A ) ) ) = ( abs ` A ) )
23 19 21 22 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` ( abs ` A ) ) ) = ( abs ` A ) )
24 16 23 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( Re ` ( log ` A ) ) ) = ( abs ` A ) )
25 14 24 oveq12d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( exp ` ( log ` A ) ) / ( exp ` ( Re ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
26 5 13 25 3eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )