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 φFV
liminflelimsup.2 φkjk+∞Fj+∞*
Assertion liminflelimsup φlim infFlim supF

Proof

Step Hyp Ref Expression
1 liminflelimsup.1 φFV
2 liminflelimsup.2 φkjk+∞Fj+∞*
3 oveq1 k=ik+∞=i+∞
4 3 rexeqdv k=ijk+∞Fj+∞*ji+∞Fj+∞*
5 oveq1 j=lj+∞=l+∞
6 5 imaeq2d j=lFj+∞=Fl+∞
7 6 ineq1d j=lFj+∞*=Fl+∞*
8 7 neeq1d j=lFj+∞*Fl+∞*
9 8 cbvrexvw ji+∞Fj+∞*li+∞Fl+∞*
10 9 a1i k=iji+∞Fj+∞*li+∞Fl+∞*
11 4 10 bitrd k=ijk+∞Fj+∞*li+∞Fl+∞*
12 11 cbvralvw kjk+∞Fj+∞*ili+∞Fl+∞*
13 2 12 sylib φili+∞Fl+∞*
14 1 13 liminflelimsuplem φlim infFlim supF