Metamath Proof Explorer

Theorem liminflelimsup

Description: The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex for a counterexample). The inequality can be strict, see liminfltlimsupex . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflelimsup.1 
|- ( ph -> F e. V )
liminflelimsup.2 
|- ( ph -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
Assertion liminflelimsup 
|- ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 liminflelimsup.1 
 |-  ( ph -> F e. V )
2 liminflelimsup.2 
 |-  ( ph -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
3 oveq1 
 |-  ( k = i -> ( k [,) +oo ) = ( i [,) +oo ) )
4 3 rexeqdv 
 |-  ( k = i -> ( E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) <-> E. j e. ( i [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) )
5 oveq1 
 |-  ( j = l -> ( j [,) +oo ) = ( l [,) +oo ) )
6 5 imaeq2d 
 |-  ( j = l -> ( F " ( j [,) +oo ) ) = ( F " ( l [,) +oo ) ) )
7 6 ineq1d 
 |-  ( j = l -> ( ( F " ( j [,) +oo ) ) i^i RR* ) = ( ( F " ( l [,) +oo ) ) i^i RR* ) )
8 7 neeq1d 
 |-  ( j = l -> ( ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) <-> ( ( F " ( l [,) +oo ) ) i^i RR* ) =/= (/) ) )
9 8 cbvrexvw 
 |-  ( E. j e. ( i [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) <-> E. l e. ( i [,) +oo ) ( ( F " ( l [,) +oo ) ) i^i RR* ) =/= (/) )
10 9 a1i 
 |-  ( k = i -> ( E. j e. ( i [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) <-> E. l e. ( i [,) +oo ) ( ( F " ( l [,) +oo ) ) i^i RR* ) =/= (/) ) )
11 4 10 bitrd 
 |-  ( k = i -> ( E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) <-> E. l e. ( i [,) +oo ) ( ( F " ( l [,) +oo ) ) i^i RR* ) =/= (/) ) )
12 11 cbvralvw 
 |-  ( A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) <-> A. i e. RR E. l e. ( i [,) +oo ) ( ( F " ( l [,) +oo ) ) i^i RR* ) =/= (/) )
13 2 12 sylib 
 |-  ( ph -> A. i e. RR E. l e. ( i [,) +oo ) ( ( F " ( l [,) +oo ) ) i^i RR* ) =/= (/) )
14 1 13 liminflelimsuplem 
 |-  ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )