# 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 ) )`