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 ) )