Metamath Proof Explorer


Theorem relogef

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

Ref Expression
Assertion relogef
|- ( A e. RR -> ( log ` ( exp ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 relogrn
 |-  ( A e. RR -> A e. ran log )
2 logef
 |-  ( A e. ran log -> ( log ` ( exp ` A ) ) = A )
3 1 2 syl
 |-  ( A e. RR -> ( log ` ( exp ` A ) ) = A )