Metamath Proof Explorer

Theorem dfrelog

Description: The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion dfrelog 
|- ( log |` RR+ ) = `' ( exp |` RR )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( ( exp |` ran log ) " RR ) = ran ( ( exp |` ran log ) |` RR )
2 relogrn 
 |-  ( x e. RR -> x e. ran log )
3 2 ssriv 
 |-  RR C_ ran log
4 resabs1 
 |-  ( RR C_ ran log -> ( ( exp |` ran log ) |` RR ) = ( exp |` RR ) )
5 3 4 ax-mp 
 |-  ( ( exp |` ran log ) |` RR ) = ( exp |` RR )
6 5 rneqi 
 |-  ran ( ( exp |` ran log ) |` RR ) = ran ( exp |` RR )
7 reeff1o 
 |-  ( exp |` RR ) : RR -1-1-onto-> RR+
8 dff1o2 
 |-  ( ( exp |` RR ) : RR -1-1-onto-> RR+ <-> ( ( exp |` RR ) Fn RR /\ Fun `' ( exp |` RR ) /\ ran ( exp |` RR ) = RR+ ) )
9 7 8 mpbi 
 |-  ( ( exp |` RR ) Fn RR /\ Fun `' ( exp |` RR ) /\ ran ( exp |` RR ) = RR+ )
10 9 simp3i 
 |-  ran ( exp |` RR ) = RR+
11 1 6 10 3eqtri 
 |-  ( ( exp |` ran log ) " RR ) = RR+
12 11 reseq2i 
 |-  ( `' ( exp |` ran log ) |` ( ( exp |` ran log ) " RR ) ) = ( `' ( exp |` ran log ) |` RR+ )
13 5 cnveqi 
 |-  `' ( ( exp |` ran log ) |` RR ) = `' ( exp |` RR )
14 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
15 f1ofun 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> Fun log )
16 14 15 ax-mp 
 |-  Fun log
17 dflog2 
 |-  log = `' ( exp |` ran log )
18 17 funeqi 
 |-  ( Fun log <-> Fun `' ( exp |` ran log ) )
19 16 18 mpbi 
 |-  Fun `' ( exp |` ran log )
20 funcnvres 
 |-  ( Fun `' ( exp |` ran log ) -> `' ( ( exp |` ran log ) |` RR ) = ( `' ( exp |` ran log ) |` ( ( exp |` ran log ) " RR ) ) )
21 19 20 ax-mp 
 |-  `' ( ( exp |` ran log ) |` RR ) = ( `' ( exp |` ran log ) |` ( ( exp |` ran log ) " RR ) )
22 13 21 eqtr3i 
 |-  `' ( exp |` RR ) = ( `' ( exp |` ran log ) |` ( ( exp |` ran log ) " RR ) )
23 17 reseq1i 
 |-  ( log |` RR+ ) = ( `' ( exp |` ran log ) |` RR+ )
24 12 22 23 3eqtr4ri 
 |-  ( log |` RR+ ) = `' ( exp |` RR )