Metamath Proof Explorer

Theorem relog

Description: Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion relog 
|- ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) = ( log ` ( 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 relogef 
 |-  ( ( Re ` ( log ` A ) ) e. RR -> ( log ` ( exp ` ( Re ` ( log ` A ) ) ) ) = ( Re ` ( log ` A ) ) )
4 2 3 syl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` ( exp ` ( Re ` ( log ` A ) ) ) ) = ( Re ` ( log ` A ) ) )
5 absef 
 |-  ( ( log ` A ) e. CC -> ( abs ` ( exp ` ( log ` A ) ) ) = ( exp ` ( Re ` ( log ` A ) ) ) )
6 1 5 syl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( exp ` ( log ` A ) ) ) = ( exp ` ( Re ` ( log ` A ) ) ) )
7 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
8 7 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( exp ` ( log ` A ) ) ) = ( abs ` A ) )
9 6 8 eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( Re ` ( log ` A ) ) ) = ( abs ` A ) )
10 9 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` ( exp ` ( Re ` ( log ` A ) ) ) ) = ( log ` ( abs ` A ) ) )
11 4 10 eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) = ( log ` ( abs ` A ) ) )