Metamath Proof Explorer

Theorem liminflelimsupuz

Description: The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflelimsupuz.1 
|- ( ph -> M e. ZZ )
liminflelimsupuz.2 
|- Z = ( ZZ>= ` M )
liminflelimsupuz.3 
|- ( ph -> F : Z --> RR* )
Assertion liminflelimsupuz 
|- ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 liminflelimsupuz.1 
 |-  ( ph -> M e. ZZ )
2 liminflelimsupuz.2 
 |-  Z = ( ZZ>= ` M )
3 liminflelimsupuz.3 
 |-  ( ph -> F : Z --> RR* )
4 2 fvexi 
 |-  Z e. _V
5 4 a1i 
 |-  ( ph -> Z e. _V )
6 3 5 fexd 
 |-  ( ph -> F e. _V )
7 1 2 uzubico2 
 |-  ( ph -> A. k e. RR E. j e. ( k [,) +oo ) j e. Z )
8 3 ffnd 
 |-  ( ph -> F Fn Z )
9 8 adantr 
 |-  ( ( ph /\ j e. Z ) -> F Fn Z )
10 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
11 id 
 |-  ( j e. Z -> j e. Z )
12 2 11 uzxrd 
 |-  ( j e. Z -> j e. RR* )
13 pnfxr 
 |-  +oo e. RR*
14 13 a1i 
 |-  ( j e. Z -> +oo e. RR* )
15 12 xrleidd 
 |-  ( j e. Z -> j <_ j )
16 2 11 uzred 
 |-  ( j e. Z -> j e. RR )
17 ltpnf 
 |-  ( j e. RR -> j < +oo )
18 16 17 syl 
 |-  ( j e. Z -> j < +oo )
19 12 14 12 15 18 elicod 
 |-  ( j e. Z -> j e. ( j [,) +oo ) )
20 19 adantl 
 |-  ( ( ph /\ j e. Z ) -> j e. ( j [,) +oo ) )
21 9 10 20 fnfvimad 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. ( F " ( j [,) +oo ) ) )
22 3 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR* )
23 21 22 elind 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. ( ( F " ( j [,) +oo ) ) i^i RR* ) )
24 23 ne0d 
 |-  ( ( ph /\ j e. Z ) -> ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
25 24 ex 
 |-  ( ph -> ( j e. Z -> ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) )
26 25 ad2antrr 
 |-  ( ( ( ph /\ k e. RR ) /\ j e. ( k [,) +oo ) ) -> ( j e. Z -> ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) )
27 26 reximdva 
 |-  ( ( ph /\ k e. RR ) -> ( E. j e. ( k [,) +oo ) j e. Z -> E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) )
28 27 ralimdva 
 |-  ( ph -> ( A. k e. RR E. j e. ( k [,) +oo ) j e. Z -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) )
29 7 28 mpd 
 |-  ( ph -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
30 6 29 liminflelimsup 
 |-  ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )