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