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 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
59 |
58
|
tgioo2 |
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
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 59 58 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 ) |