Metamath Proof Explorer


Theorem dvrelog2

Description: The derivative of the logarithm, ftc2 version. (Contributed by metakunt, 11-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 dvrelog2.1
 |-  ( ph -> A e. RR )
2 dvrelog2.2
 |-  ( ph -> B e. RR )
3 dvrelog2.3
 |-  ( ph -> 0 < A )
4 dvrelog2.4
 |-  ( ph -> A <_ B )
5 dvrelog2.5
 |-  F = ( x e. ( A [,] B ) |-> ( log ` x ) )
6 dvrelog2.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 rpssre
 |-  RR+ C_ RR
12 ax-resscn
 |-  RR C_ CC
13 11 12 sstri
 |-  RR+ C_ CC
14 13 sseli
 |-  ( x e. RR+ -> x e. CC )
15 14 adantl
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
16 rpne0
 |-  ( x e. RR+ -> x =/= 0 )
17 16 adantl
 |-  ( ( ph /\ x e. RR+ ) -> x =/= 0 )
18 15 17 logcld
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
19 1red
 |-  ( x e. RR+ -> 1 e. RR )
20 11 sseli
 |-  ( x e. RR+ -> x e. RR )
21 19 20 16 redivcld
 |-  ( x e. RR+ -> ( 1 / x ) e. RR )
22 21 adantl
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) e. RR )
23 logf1o
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
24 f1of
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
25 23 24 ax-mp
 |-  log : ( CC \ { 0 } ) --> ran log
26 25 a1i
 |-  ( ph -> log : ( CC \ { 0 } ) --> ran log )
27 0nrp
 |-  -. 0 e. RR+
28 disjsn
 |-  ( ( RR+ i^i { 0 } ) = (/) <-> -. 0 e. RR+ )
29 27 28 mpbir
 |-  ( RR+ i^i { 0 } ) = (/)
30 disjdif2
 |-  ( ( RR+ i^i { 0 } ) = (/) -> ( RR+ \ { 0 } ) = RR+ )
31 29 30 ax-mp
 |-  ( RR+ \ { 0 } ) = RR+
32 ssdif
 |-  ( RR+ C_ CC -> ( RR+ \ { 0 } ) C_ ( CC \ { 0 } ) )
33 13 32 ax-mp
 |-  ( RR+ \ { 0 } ) C_ ( CC \ { 0 } )
34 31 33 eqsstrri
 |-  RR+ C_ ( CC \ { 0 } )
35 34 a1i
 |-  ( ph -> RR+ C_ ( CC \ { 0 } ) )
36 26 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 elicc2
 |-  ( ( 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 1 adantr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> A e. RR )
48 3 adantr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> 0 < A )
49 44 simp2d
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> A <_ y )
50 46 47 45 48 49 ltletrd
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> 0 < y )
51 45 50 jca
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. RR /\ 0 < y ) )
52 elrp
 |-  ( y e. RR+ <-> ( y e. RR /\ 0 < y ) )
53 51 52 sylibr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> y e. RR+ )
54 53 ex
 |-  ( ph -> ( y e. ( A [,] B ) -> y e. RR+ ) )
55 54 ssrdv
 |-  ( ph -> ( A [,] B ) C_ RR+ )
56 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
57 56 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
58 iccntr
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
59 1 2 58 syl2anc
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
60 10 18 22 41 55 57 56 59 dvmptres2
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( log ` x ) ) ) = ( x e. ( A (,) B ) |-> ( 1 / x ) ) )
61 8 60 eqtrd
 |-  ( ph -> ( RR _D F ) = ( x e. ( A (,) B ) |-> ( 1 / x ) ) )
62 6 a1i
 |-  ( ph -> G = ( x e. ( A (,) B ) |-> ( 1 / x ) ) )
63 62 eqcomd
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( 1 / x ) ) = G )
64 61 63 eqtrd
 |-  ( ph -> ( RR _D F ) = G )