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 )