This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )