Metamath Proof Explorer

Theorem reeflog

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

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

Proof

Step Hyp Ref Expression
1 rpcnne0 
 |-  ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
2 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
3 1 2 syl 
 |-  ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )