Metamath Proof Explorer


Theorem relogeftb

Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Assertion relogeftb
|- ( ( A e. RR+ /\ B e. RR ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )

Proof

Step Hyp Ref Expression
1 rpcnne0
 |-  ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
2 relogrn
 |-  ( B e. RR -> B e. ran log )
3 logeftb
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )
4 3 3expa
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )
5 1 2 4 syl2an
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )