This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem liminflelimsupcex

Description: A counterexample for liminflelimsup , showing that the second hypothesis is needed. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion liminflelimsupcex ( lim sup ‘ ∅ ) < ( lim inf ‘ ∅ )

Proof

Step Hyp Ref Expression
1 mnfltpnf ⊢ -∞ < +∞
2 limsup0 ⊢ ( lim sup ‘ ∅ ) = -∞
3 liminf0 ⊢ ( lim inf ‘ ∅ ) = +∞
4 2 3 breq12i ⊢ ( ( lim sup ‘ ∅ ) < ( lim inf ‘ ∅ ) ↔ -∞ < +∞ )
5 1 4 mpbir ⊢ ( lim sup ‘ ∅ ) < ( lim inf ‘ ∅ )