| Step |
Hyp |
Ref |
Expression |
| 1 |
|
nftru |
|- F/ x T. |
| 2 |
|
0ex |
|- (/) e. _V |
| 3 |
2
|
a1i |
|- ( T. -> (/) e. _V ) |
| 4 |
|
0red |
|- ( T. -> 0 e. RR ) |
| 5 |
|
noel |
|- -. x e. (/) |
| 6 |
|
elinel1 |
|- ( x e. ( (/) i^i ( 0 [,) +oo ) ) -> x e. (/) ) |
| 7 |
6
|
con3i |
|- ( -. x e. (/) -> -. x e. ( (/) i^i ( 0 [,) +oo ) ) ) |
| 8 |
5 7
|
ax-mp |
|- -. x e. ( (/) i^i ( 0 [,) +oo ) ) |
| 9 |
|
pm2.21 |
|- ( -. x e. ( (/) i^i ( 0 [,) +oo ) ) -> ( x e. ( (/) i^i ( 0 [,) +oo ) ) -> ( (/) ` x ) e. RR* ) ) |
| 10 |
8 9
|
ax-mp |
|- ( x e. ( (/) i^i ( 0 [,) +oo ) ) -> ( (/) ` x ) e. RR* ) |
| 11 |
10
|
adantl |
|- ( ( T. /\ x e. ( (/) i^i ( 0 [,) +oo ) ) ) -> ( (/) ` x ) e. RR* ) |
| 12 |
1 3 4 11
|
liminfval3 |
|- ( T. -> ( liminf ` ( x e. (/) |-> ( (/) ` x ) ) ) = -e ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) ) |
| 13 |
12
|
mptru |
|- ( liminf ` ( x e. (/) |-> ( (/) ` x ) ) ) = -e ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) |
| 14 |
|
mpt0 |
|- ( x e. (/) |-> ( (/) ` x ) ) = (/) |
| 15 |
14
|
fveq2i |
|- ( liminf ` ( x e. (/) |-> ( (/) ` x ) ) ) = ( liminf ` (/) ) |
| 16 |
|
mpt0 |
|- ( x e. (/) |-> -e ( (/) ` x ) ) = (/) |
| 17 |
16
|
fveq2i |
|- ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) = ( limsup ` (/) ) |
| 18 |
|
limsup0 |
|- ( limsup ` (/) ) = -oo |
| 19 |
17 18
|
eqtri |
|- ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) = -oo |
| 20 |
19
|
xnegeqi |
|- -e ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) = -e -oo |
| 21 |
|
xnegmnf |
|- -e -oo = +oo |
| 22 |
20 21
|
eqtri |
|- -e ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) = +oo |
| 23 |
13 15 22
|
3eqtr3i |
|- ( liminf ` (/) ) = +oo |