Step |
Hyp |
Ref |
Expression |
1 |
|
xrge0iifhmeo.1 |
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) ) |
2 |
|
iccssxr |
|- ( 0 [,] 1 ) C_ RR* |
3 |
|
xrltso |
|- < Or RR* |
4 |
|
soss |
|- ( ( 0 [,] 1 ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] 1 ) ) ) |
5 |
2 3 4
|
mp2 |
|- < Or ( 0 [,] 1 ) |
6 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
7 |
|
cnvso |
|- ( < Or RR* <-> `' < Or RR* ) |
8 |
3 7
|
mpbi |
|- `' < Or RR* |
9 |
|
sopo |
|- ( `' < Or RR* -> `' < Po RR* ) |
10 |
8 9
|
ax-mp |
|- `' < Po RR* |
11 |
|
poss |
|- ( ( 0 [,] +oo ) C_ RR* -> ( `' < Po RR* -> `' < Po ( 0 [,] +oo ) ) ) |
12 |
6 10 11
|
mp2 |
|- `' < Po ( 0 [,] +oo ) |
13 |
1
|
xrge0iifcnv |
|- ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( z e. ( 0 [,] +oo ) |-> if ( z = +oo , 0 , ( exp ` -u z ) ) ) ) |
14 |
13
|
simpli |
|- F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) |
15 |
|
f1ofo |
|- ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) -> F : ( 0 [,] 1 ) -onto-> ( 0 [,] +oo ) ) |
16 |
14 15
|
ax-mp |
|- F : ( 0 [,] 1 ) -onto-> ( 0 [,] +oo ) |
17 |
|
0xr |
|- 0 e. RR* |
18 |
|
1xr |
|- 1 e. RR* |
19 |
|
0le1 |
|- 0 <_ 1 |
20 |
|
snunioc |
|- ( ( 0 e. RR* /\ 1 e. RR* /\ 0 <_ 1 ) -> ( { 0 } u. ( 0 (,] 1 ) ) = ( 0 [,] 1 ) ) |
21 |
17 18 19 20
|
mp3an |
|- ( { 0 } u. ( 0 (,] 1 ) ) = ( 0 [,] 1 ) |
22 |
21
|
eleq2i |
|- ( w e. ( { 0 } u. ( 0 (,] 1 ) ) <-> w e. ( 0 [,] 1 ) ) |
23 |
|
elun |
|- ( w e. ( { 0 } u. ( 0 (,] 1 ) ) <-> ( w e. { 0 } \/ w e. ( 0 (,] 1 ) ) ) |
24 |
22 23
|
bitr3i |
|- ( w e. ( 0 [,] 1 ) <-> ( w e. { 0 } \/ w e. ( 0 (,] 1 ) ) ) |
25 |
|
velsn |
|- ( w e. { 0 } <-> w = 0 ) |
26 |
|
elunitrn |
|- ( z e. ( 0 [,] 1 ) -> z e. RR ) |
27 |
26
|
adantr |
|- ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> z e. RR ) |
28 |
|
simpr |
|- ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> 0 < z ) |
29 |
|
elicc01 |
|- ( z e. ( 0 [,] 1 ) <-> ( z e. RR /\ 0 <_ z /\ z <_ 1 ) ) |
30 |
29
|
simp3bi |
|- ( z e. ( 0 [,] 1 ) -> z <_ 1 ) |
31 |
30
|
adantr |
|- ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> z <_ 1 ) |
32 |
|
1re |
|- 1 e. RR |
33 |
|
elioc2 |
|- ( ( 0 e. RR* /\ 1 e. RR ) -> ( z e. ( 0 (,] 1 ) <-> ( z e. RR /\ 0 < z /\ z <_ 1 ) ) ) |
34 |
17 32 33
|
mp2an |
|- ( z e. ( 0 (,] 1 ) <-> ( z e. RR /\ 0 < z /\ z <_ 1 ) ) |
35 |
27 28 31 34
|
syl3anbrc |
|- ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> z e. ( 0 (,] 1 ) ) |
36 |
|
pnfxr |
|- +oo e. RR* |
37 |
|
0le0 |
|- 0 <_ 0 |
38 |
|
ltpnf |
|- ( 1 e. RR -> 1 < +oo ) |
39 |
32 38
|
ax-mp |
|- 1 < +oo |
40 |
|
iocssioo |
|- ( ( ( 0 e. RR* /\ +oo e. RR* ) /\ ( 0 <_ 0 /\ 1 < +oo ) ) -> ( 0 (,] 1 ) C_ ( 0 (,) +oo ) ) |
41 |
17 36 37 39 40
|
mp4an |
|- ( 0 (,] 1 ) C_ ( 0 (,) +oo ) |
42 |
|
ioorp |
|- ( 0 (,) +oo ) = RR+ |
43 |
41 42
|
sseqtri |
|- ( 0 (,] 1 ) C_ RR+ |
44 |
43
|
sseli |
|- ( z e. ( 0 (,] 1 ) -> z e. RR+ ) |
45 |
|
relogcl |
|- ( z e. RR+ -> ( log ` z ) e. RR ) |
46 |
45
|
renegcld |
|- ( z e. RR+ -> -u ( log ` z ) e. RR ) |
47 |
|
ltpnf |
|- ( -u ( log ` z ) e. RR -> -u ( log ` z ) < +oo ) |
48 |
46 47
|
syl |
|- ( z e. RR+ -> -u ( log ` z ) < +oo ) |
49 |
|
brcnvg |
|- ( ( +oo e. RR* /\ -u ( log ` z ) e. RR ) -> ( +oo `' < -u ( log ` z ) <-> -u ( log ` z ) < +oo ) ) |
50 |
36 46 49
|
sylancr |
|- ( z e. RR+ -> ( +oo `' < -u ( log ` z ) <-> -u ( log ` z ) < +oo ) ) |
51 |
48 50
|
mpbird |
|- ( z e. RR+ -> +oo `' < -u ( log ` z ) ) |
52 |
44 51
|
syl |
|- ( z e. ( 0 (,] 1 ) -> +oo `' < -u ( log ` z ) ) |
53 |
1
|
xrge0iifcv |
|- ( z e. ( 0 (,] 1 ) -> ( F ` z ) = -u ( log ` z ) ) |
54 |
52 53
|
breqtrrd |
|- ( z e. ( 0 (,] 1 ) -> +oo `' < ( F ` z ) ) |
55 |
35 54
|
syl |
|- ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> +oo `' < ( F ` z ) ) |
56 |
55
|
ex |
|- ( z e. ( 0 [,] 1 ) -> ( 0 < z -> +oo `' < ( F ` z ) ) ) |
57 |
|
breq1 |
|- ( w = 0 -> ( w < z <-> 0 < z ) ) |
58 |
|
fveq2 |
|- ( w = 0 -> ( F ` w ) = ( F ` 0 ) ) |
59 |
|
0elunit |
|- 0 e. ( 0 [,] 1 ) |
60 |
|
iftrue |
|- ( x = 0 -> if ( x = 0 , +oo , -u ( log ` x ) ) = +oo ) |
61 |
|
pnfex |
|- +oo e. _V |
62 |
60 1 61
|
fvmpt |
|- ( 0 e. ( 0 [,] 1 ) -> ( F ` 0 ) = +oo ) |
63 |
59 62
|
ax-mp |
|- ( F ` 0 ) = +oo |
64 |
58 63
|
eqtrdi |
|- ( w = 0 -> ( F ` w ) = +oo ) |
65 |
64
|
breq1d |
|- ( w = 0 -> ( ( F ` w ) `' < ( F ` z ) <-> +oo `' < ( F ` z ) ) ) |
66 |
57 65
|
imbi12d |
|- ( w = 0 -> ( ( w < z -> ( F ` w ) `' < ( F ` z ) ) <-> ( 0 < z -> +oo `' < ( F ` z ) ) ) ) |
67 |
56 66
|
syl5ibr |
|- ( w = 0 -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) ) |
68 |
25 67
|
sylbi |
|- ( w e. { 0 } -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) ) |
69 |
|
simpll |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> w e. ( 0 (,] 1 ) ) |
70 |
26
|
ad2antlr |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> z e. RR ) |
71 |
|
0re |
|- 0 e. RR |
72 |
71
|
a1i |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> 0 e. RR ) |
73 |
43
|
sseli |
|- ( w e. ( 0 (,] 1 ) -> w e. RR+ ) |
74 |
73
|
rpred |
|- ( w e. ( 0 (,] 1 ) -> w e. RR ) |
75 |
74
|
ad2antrr |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> w e. RR ) |
76 |
|
elioc2 |
|- ( ( 0 e. RR* /\ 1 e. RR ) -> ( w e. ( 0 (,] 1 ) <-> ( w e. RR /\ 0 < w /\ w <_ 1 ) ) ) |
77 |
17 32 76
|
mp2an |
|- ( w e. ( 0 (,] 1 ) <-> ( w e. RR /\ 0 < w /\ w <_ 1 ) ) |
78 |
77
|
simp2bi |
|- ( w e. ( 0 (,] 1 ) -> 0 < w ) |
79 |
78
|
ad2antrr |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> 0 < w ) |
80 |
|
simpr |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> w < z ) |
81 |
72 75 70 79 80
|
lttrd |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> 0 < z ) |
82 |
30
|
ad2antlr |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> z <_ 1 ) |
83 |
70 81 82 34
|
syl3anbrc |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> z e. ( 0 (,] 1 ) ) |
84 |
69 83
|
jca |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) ) |
85 |
73
|
adantr |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> w e. RR+ ) |
86 |
85
|
relogcld |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( log ` w ) e. RR ) |
87 |
44
|
adantl |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> z e. RR+ ) |
88 |
87
|
relogcld |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( log ` z ) e. RR ) |
89 |
86 88
|
ltnegd |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( ( log ` w ) < ( log ` z ) <-> -u ( log ` z ) < -u ( log ` w ) ) ) |
90 |
|
logltb |
|- ( ( w e. RR+ /\ z e. RR+ ) -> ( w < z <-> ( log ` w ) < ( log ` z ) ) ) |
91 |
73 44 90
|
syl2an |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( w < z <-> ( log ` w ) < ( log ` z ) ) ) |
92 |
|
negex |
|- -u ( log ` w ) e. _V |
93 |
|
negex |
|- -u ( log ` z ) e. _V |
94 |
92 93
|
brcnv |
|- ( -u ( log ` w ) `' < -u ( log ` z ) <-> -u ( log ` z ) < -u ( log ` w ) ) |
95 |
94
|
a1i |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( -u ( log ` w ) `' < -u ( log ` z ) <-> -u ( log ` z ) < -u ( log ` w ) ) ) |
96 |
89 91 95
|
3bitr4d |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( w < z <-> -u ( log ` w ) `' < -u ( log ` z ) ) ) |
97 |
96
|
biimpd |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( w < z -> -u ( log ` w ) `' < -u ( log ` z ) ) ) |
98 |
1
|
xrge0iifcv |
|- ( w e. ( 0 (,] 1 ) -> ( F ` w ) = -u ( log ` w ) ) |
99 |
98 53
|
breqan12d |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( ( F ` w ) `' < ( F ` z ) <-> -u ( log ` w ) `' < -u ( log ` z ) ) ) |
100 |
97 99
|
sylibrd |
|- ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) |
101 |
84 80 100
|
sylc |
|- ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> ( F ` w ) `' < ( F ` z ) ) |
102 |
101
|
exp31 |
|- ( w e. ( 0 (,] 1 ) -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) ) |
103 |
68 102
|
jaoi |
|- ( ( w e. { 0 } \/ w e. ( 0 (,] 1 ) ) -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) ) |
104 |
24 103
|
sylbi |
|- ( w e. ( 0 [,] 1 ) -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) ) |
105 |
104
|
imp |
|- ( ( w e. ( 0 [,] 1 ) /\ z e. ( 0 [,] 1 ) ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) |
106 |
105
|
rgen2 |
|- A. w e. ( 0 [,] 1 ) A. z e. ( 0 [,] 1 ) ( w < z -> ( F ` w ) `' < ( F ` z ) ) |
107 |
|
soisoi |
|- ( ( ( < Or ( 0 [,] 1 ) /\ `' < Po ( 0 [,] +oo ) ) /\ ( F : ( 0 [,] 1 ) -onto-> ( 0 [,] +oo ) /\ A. w e. ( 0 [,] 1 ) A. z e. ( 0 [,] 1 ) ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) ) -> F Isom < , `' < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) ) |
108 |
5 12 16 106 107
|
mp4an |
|- F Isom < , `' < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) |