Metamath Proof Explorer

Theorem dvrelog

Description: The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Assertion dvrelog 
|- ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )

Proof

Step Hyp Ref Expression
1 dfrelog 
 |-  ( log |` RR+ ) = `' ( exp |` RR )
2 1 oveq2i 
 |-  ( RR _D ( log |` RR+ ) ) = ( RR _D `' ( exp |` RR ) )
3 reeff1o 
 |-  ( exp |` RR ) : RR -1-1-onto-> RR+
4 f1of 
 |-  ( ( exp |` RR ) : RR -1-1-onto-> RR+ -> ( exp |` RR ) : RR --> RR+ )
5 3 4 ax-mp 
 |-  ( exp |` RR ) : RR --> RR+
6 rpssre 
 |-  RR+ C_ RR
7 fss 
 |-  ( ( ( exp |` RR ) : RR --> RR+ /\ RR+ C_ RR ) -> ( exp |` RR ) : RR --> RR )
8 5 6 7 mp2an 
 |-  ( exp |` RR ) : RR --> RR
9 ax-resscn 
 |-  RR C_ CC
10 efcn 
 |-  exp e. ( CC -cn-> CC )
11 rescncf 
 |-  ( RR C_ CC -> ( exp e. ( CC -cn-> CC ) -> ( exp |` RR ) e. ( RR -cn-> CC ) ) )
12 9 10 11 mp2 
 |-  ( exp |` RR ) e. ( RR -cn-> CC )
13 cncffvrn 
 |-  ( ( RR C_ CC /\ ( exp |` RR ) e. ( RR -cn-> CC ) ) -> ( ( exp |` RR ) e. ( RR -cn-> RR ) <-> ( exp |` RR ) : RR --> RR ) )
14 9 12 13 mp2an 
 |-  ( ( exp |` RR ) e. ( RR -cn-> RR ) <-> ( exp |` RR ) : RR --> RR )
15 8 14 mpbir 
 |-  ( exp |` RR ) e. ( RR -cn-> RR )
16 15 a1i 
 |-  ( T. -> ( exp |` RR ) e. ( RR -cn-> RR ) )
17 reelprrecn 
 |-  RR e. { RR , CC }
18 eff 
 |-  exp : CC --> CC
19 ssid 
 |-  CC C_ CC
20 dvef 
 |-  ( CC _D exp ) = exp
21 20 dmeqi 
 |-  dom ( CC _D exp ) = dom exp
22 18 fdmi 
 |-  dom exp = CC
23 21 22 eqtri 
 |-  dom ( CC _D exp ) = CC
24 9 23 sseqtrri 
 |-  RR C_ dom ( CC _D exp )
25 dvres3 
 |-  ( ( ( RR e. { RR , CC } /\ exp : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D exp ) ) ) -> ( RR _D ( exp |` RR ) ) = ( ( CC _D exp ) |` RR ) )
26 17 18 19 24 25 mp4an 
 |-  ( RR _D ( exp |` RR ) ) = ( ( CC _D exp ) |` RR )
27 20 reseq1i 
 |-  ( ( CC _D exp ) |` RR ) = ( exp |` RR )
28 26 27 eqtri 
 |-  ( RR _D ( exp |` RR ) ) = ( exp |` RR )
29 28 dmeqi 
 |-  dom ( RR _D ( exp |` RR ) ) = dom ( exp |` RR )
30 5 fdmi 
 |-  dom ( exp |` RR ) = RR
31 29 30 eqtri 
 |-  dom ( RR _D ( exp |` RR ) ) = RR
32 31 a1i 
 |-  ( T. -> dom ( RR _D ( exp |` RR ) ) = RR )
33 0nrp 
 |-  -. 0 e. RR+
34 28 rneqi 
 |-  ran ( RR _D ( exp |` RR ) ) = ran ( exp |` RR )
35 f1ofo 
 |-  ( ( exp |` RR ) : RR -1-1-onto-> RR+ -> ( exp |` RR ) : RR -onto-> RR+ )
36 forn 
 |-  ( ( exp |` RR ) : RR -onto-> RR+ -> ran ( exp |` RR ) = RR+ )
37 3 35 36 mp2b 
 |-  ran ( exp |` RR ) = RR+
38 34 37 eqtri 
 |-  ran ( RR _D ( exp |` RR ) ) = RR+
39 38 eleq2i 
 |-  ( 0 e. ran ( RR _D ( exp |` RR ) ) <-> 0 e. RR+ )
40 33 39 mtbir 
 |-  -. 0 e. ran ( RR _D ( exp |` RR ) )
41 40 a1i 
 |-  ( T. -> -. 0 e. ran ( RR _D ( exp |` RR ) ) )
42 3 a1i 
 |-  ( T. -> ( exp |` RR ) : RR -1-1-onto-> RR+ )
43 16 32 41 42 dvcnvre 
 |-  ( T. -> ( RR _D `' ( exp |` RR ) ) = ( x e. RR+ |-> ( 1 / ( ( RR _D ( exp |` RR ) ) ` ( `' ( exp |` RR ) ` x ) ) ) ) )
44 43 mptru 
 |-  ( RR _D `' ( exp |` RR ) ) = ( x e. RR+ |-> ( 1 / ( ( RR _D ( exp |` RR ) ) ` ( `' ( exp |` RR ) ` x ) ) ) )
45 28 fveq1i 
 |-  ( ( RR _D ( exp |` RR ) ) ` ( `' ( exp |` RR ) ` x ) ) = ( ( exp |` RR ) ` ( `' ( exp |` RR ) ` x ) )
46 f1ocnvfv2 
 |-  ( ( ( exp |` RR ) : RR -1-1-onto-> RR+ /\ x e. RR+ ) -> ( ( exp |` RR ) ` ( `' ( exp |` RR ) ` x ) ) = x )
47 3 46 mpan 
 |-  ( x e. RR+ -> ( ( exp |` RR ) ` ( `' ( exp |` RR ) ` x ) ) = x )
48 45 47 syl5eq 
 |-  ( x e. RR+ -> ( ( RR _D ( exp |` RR ) ) ` ( `' ( exp |` RR ) ` x ) ) = x )
49 48 oveq2d 
 |-  ( x e. RR+ -> ( 1 / ( ( RR _D ( exp |` RR ) ) ` ( `' ( exp |` RR ) ` x ) ) ) = ( 1 / x ) )
50 49 mpteq2ia 
 |-  ( x e. RR+ |-> ( 1 / ( ( RR _D ( exp |` RR ) ) ` ( `' ( exp |` RR ) ` x ) ) ) ) = ( x e. RR+ |-> ( 1 / x ) )
51 44 50 eqtri 
 |-  ( RR _D `' ( exp |` RR ) ) = ( x e. RR+ |-> ( 1 / x ) )
52 2 51 eqtri 
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )