Metamath Proof Explorer

Theorem logef

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

Ref Expression
Assertion logef 
|- ( A e. ran log -> ( log ` ( exp ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 dflog2 
 |-  log = `' ( exp |` ran log )
2 1 fveq1i 
 |-  ( log ` ( ( exp |` ran log ) ` A ) ) = ( `' ( exp |` ran log ) ` ( ( exp |` ran log ) ` A ) )
3 fvres 
 |-  ( A e. ran log -> ( ( exp |` ran log ) ` A ) = ( exp ` A ) )
4 3 fveq2d 
 |-  ( A e. ran log -> ( log ` ( ( exp |` ran log ) ` A ) ) = ( log ` ( exp ` A ) ) )
5 eff1o2 
 |-  ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } )
6 f1ocnvfv1 
 |-  ( ( ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) /\ A e. ran log ) -> ( `' ( exp |` ran log ) ` ( ( exp |` ran log ) ` A ) ) = A )
7 5 6 mpan 
 |-  ( A e. ran log -> ( `' ( exp |` ran log ) ` ( ( exp |` ran log ) ` A ) ) = A )
8 2 4 7 3eqtr3a 
 |-  ( A e. ran log -> ( log ` ( exp ` A ) ) = A )