Metamath Proof Explorer

Theorem dvrelog3

Description: The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024)

Ref Expression
Hypotheses dvrelog3.1 
|- ( ph -> A e. RR* )
dvrelog3.2 
|- ( ph -> B e. RR* )
dvrelog3.3 
|- ( ph -> 0 <_ A )
dvrelog3.4 
|- ( ph -> A <_ B )
dvrelog3.5 
|- F = ( x e. ( A (,) B ) |-> ( log ` x ) )
dvrelog3.6 
|- G = ( x e. ( A (,) B ) |-> ( 1 / x ) )
Assertion dvrelog3 
|- ( ph -> ( RR _D F ) = G )

Proof

Step Hyp Ref Expression
1 dvrelog3.1 
 |-  ( ph -> A e. RR* )
2 dvrelog3.2 
 |-  ( ph -> B e. RR* )
3 dvrelog3.3 
 |-  ( ph -> 0 <_ A )
4 dvrelog3.4 
 |-  ( ph -> A <_ B )
5 dvrelog3.5 
 |-  F = ( x e. ( A (,) B ) |-> ( log ` x ) )
6 dvrelog3.6 
 |-  G = ( x e. ( A (,) B ) |-> ( 1 / x ) )
7 5 a1i 
 |-  ( ph -> F = ( x e. ( A (,) B ) |-> ( log ` x ) ) )
8 7 oveq2d 
 |-  ( ph -> ( RR _D F ) = ( RR _D ( x e. ( A (,) B ) |-> ( log ` x ) ) ) )
9 reelprrecn 
 |-  RR e. { RR , CC }
10 9 a1i 
 |-  ( ph -> RR e. { RR , CC } )
11 rpcn 
 |-  ( x e. RR+ -> x e. CC )
12 11 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
13 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
14 13 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x =/= 0 )
15 12 14 logcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
16 1red 
 |-  ( ( ph /\ x e. RR+ ) -> 1 e. RR )
17 rpre 
 |-  ( x e. RR+ -> x e. RR )
18 17 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
19 16 18 14 redivcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) e. RR )
20 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
21 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
22 20 21 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
23 22 a1i 
 |-  ( ph -> log : ( CC \ { 0 } ) --> ran log )
24 0nrp 
 |-  -. 0 e. RR+
25 disjsn 
 |-  ( ( RR+ i^i { 0 } ) = (/) <-> -. 0 e. RR+ )
26 24 25 mpbir 
 |-  ( RR+ i^i { 0 } ) = (/)
27 disjdif2 
 |-  ( ( RR+ i^i { 0 } ) = (/) -> ( RR+ \ { 0 } ) = RR+ )
28 26 27 ax-mp 
 |-  ( RR+ \ { 0 } ) = RR+
29 rpssre 
 |-  RR+ C_ RR
30 ax-resscn 
 |-  RR C_ CC
31 29 30 sstri 
 |-  RR+ C_ CC
32 ssdif 
 |-  ( RR+ C_ CC -> ( RR+ \ { 0 } ) C_ ( CC \ { 0 } ) )
33 31 32 ax-mp 
 |-  ( RR+ \ { 0 } ) C_ ( CC \ { 0 } )
34 28 33 eqsstrri 
 |-  RR+ C_ ( CC \ { 0 } )
35 34 a1i 
 |-  ( ph -> RR+ C_ ( CC \ { 0 } ) )
36 23 35 feqresmpt 
 |-  ( ph -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
37 36 eqcomd 
 |-  ( ph -> ( x e. RR+ |-> ( log ` x ) ) = ( log |` RR+ ) )
38 37 oveq2d 
 |-  ( ph -> ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) = ( RR _D ( log |` RR+ ) ) )
39 dvrelog 
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
40 39 a1i 
 |-  ( ph -> ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
41 38 40 eqtrd 
 |-  ( ph -> ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
42 elioo2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( y e. ( A (,) B ) <-> ( y e. RR /\ A < y /\ y < B ) ) )
43 1 2 42 syl2anc 
 |-  ( ph -> ( y e. ( A (,) B ) <-> ( y e. RR /\ A < y /\ y < B ) ) )
44 43 biimpa 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( y e. RR /\ A < y /\ y < B ) )
45 44 simp1d 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. RR )
46 0red 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 0 e. RR )
47 46 rexrd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 0 e. RR* )
48 1 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> A e. RR* )
49 45 rexrd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. RR* )
50 3 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 0 <_ A )
51 44 simp2d 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> A < y )
52 47 48 49 50 51 xrlelttrd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> 0 < y )
53 45 52 jca 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( y e. RR /\ 0 < y ) )
54 elrp 
 |-  ( y e. RR+ <-> ( y e. RR /\ 0 < y ) )
55 53 54 sylibr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. RR+ )
56 55 ex 
 |-  ( ph -> ( y e. ( A (,) B ) -> y e. RR+ ) )
57 56 ssrdv 
 |-  ( ph -> ( A (,) B ) C_ RR+ )
58 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
59 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
60 retop 
 |-  ( topGen ` ran (,) ) e. Top
61 60 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. Top )
62 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
63 62 a1i 
 |-  ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
64 isopn3i 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) )
65 61 63 64 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) )
66 10 15 19 41 57 58 59 65 dvmptres2 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( log ` x ) ) ) = ( x e. ( A (,) B ) |-> ( 1 / x ) ) )
67 8 66 eqtrd 
 |-  ( ph -> ( RR _D F ) = ( x e. ( A (,) B ) |-> ( 1 / x ) ) )
68 6 a1i 
 |-  ( ph -> G = ( x e. ( A (,) B ) |-> ( 1 / x ) ) )
69 68 eqcomd 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( 1 / x ) ) = G )
70 67 69 eqtrd 
 |-  ( ph -> ( RR _D F ) = G )