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 + = exp -1

Proof

Step Hyp Ref Expression
1 df-ima exp ran log = ran exp ran log
2 relogrn x x ran log
3 2 ssriv ran log
4 resabs1 ran log exp ran log = exp
5 3 4 ax-mp exp ran log = exp
6 5 rneqi ran exp ran log = ran exp
7 reeff1o exp : 1-1 onto +
8 dff1o2 exp : 1-1 onto + exp Fn Fun exp -1 ran exp = +
9 7 8 mpbi exp Fn Fun exp -1 ran exp = +
10 9 simp3i ran exp = +
11 1 6 10 3eqtri exp ran log = +
12 11 reseq2i exp ran log -1 exp ran log = exp ran log -1 +
13 5 cnveqi exp ran log -1 = exp -1
14 logf1o log : 0 1-1 onto ran log
15 f1ofun log : 0 1-1 onto ran log Fun log
16 14 15 ax-mp Fun log
17 dflog2 log = exp ran log -1
18 17 funeqi Fun log Fun exp ran log -1
19 16 18 mpbi Fun exp ran log -1
20 funcnvres Fun exp ran log -1 exp ran log -1 = exp ran log -1 exp ran log
21 19 20 ax-mp exp ran log -1 = exp ran log -1 exp ran log
22 13 21 eqtr3i exp -1 = exp ran log -1 exp ran log
23 17 reseq1i log + = exp ran log -1 +
24 12 22 23 3eqtr4ri log + = exp -1