Metamath Proof Explorer

Theorem eflog

Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion eflog 
|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 dflog2 
 |-  log = `' ( exp |` ran log )
2 1 fveq1i 
 |-  ( log ` A ) = ( `' ( exp |` ran log ) ` A )
3 2 fveq2i 
 |-  ( ( exp |` ran log ) ` ( log ` A ) ) = ( ( exp |` ran log ) ` ( `' ( exp |` ran log ) ` A ) )
4 logrncl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log )
5 4 fvresd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( exp |` ran log ) ` ( log ` A ) ) = ( exp ` ( log ` A ) ) )
6 eldifsn 
 |-  ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
7 eff1o2 
 |-  ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } )
8 f1ocnvfv2 
 |-  ( ( ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) /\ A e. ( CC \ { 0 } ) ) -> ( ( exp |` ran log ) ` ( `' ( exp |` ran log ) ` A ) ) = A )
9 7 8 mpan 
 |-  ( A e. ( CC \ { 0 } ) -> ( ( exp |` ran log ) ` ( `' ( exp |` ran log ) ` A ) ) = A )
10 6 9 sylbir 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( exp |` ran log ) ` ( `' ( exp |` ran log ) ` A ) ) = A )
11 3 5 10 3eqtr3a 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )