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 ) |