Metamath Proof Explorer

Theorem logeftb

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

Ref Expression
Assertion logeftb 
|- ( ( A e. CC /\ A =/= 0 /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
2 dflog2 
 |-  log = `' ( exp |` ran log )
3 2 fveq1i 
 |-  ( log ` A ) = ( `' ( exp |` ran log ) ` A )
4 3 eqeq1i 
 |-  ( ( log ` A ) = B <-> ( `' ( exp |` ran log ) ` A ) = B )
5 fvres 
 |-  ( B e. ran log -> ( ( exp |` ran log ) ` B ) = ( exp ` B ) )
6 5 eqeq1d 
 |-  ( B e. ran log -> ( ( ( exp |` ran log ) ` B ) = A <-> ( exp ` B ) = A ) )
7 6 adantr 
 |-  ( ( B e. ran log /\ A e. ( CC \ { 0 } ) ) -> ( ( ( exp |` ran log ) ` B ) = A <-> ( exp ` B ) = A ) )
8 eff1o2 
 |-  ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } )
9 f1ocnvfvb 
 |-  ( ( ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) /\ B e. ran log /\ A e. ( CC \ { 0 } ) ) -> ( ( ( exp |` ran log ) ` B ) = A <-> ( `' ( exp |` ran log ) ` A ) = B ) )
10 8 9 mp3an1 
 |-  ( ( B e. ran log /\ A e. ( CC \ { 0 } ) ) -> ( ( ( exp |` ran log ) ` B ) = A <-> ( `' ( exp |` ran log ) ` A ) = B ) )
11 7 10 bitr3d 
 |-  ( ( B e. ran log /\ A e. ( CC \ { 0 } ) ) -> ( ( exp ` B ) = A <-> ( `' ( exp |` ran log ) ` A ) = B ) )
12 11 ancoms 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. ran log ) -> ( ( exp ` B ) = A <-> ( `' ( exp |` ran log ) ` A ) = B ) )
13 4 12 bitr4id 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )
14 1 13 sylanbr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )
15 14 3impa 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )