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 
|- ( limsup ` (/) ) < ( liminf ` (/) )

Proof

Step Hyp Ref Expression
1 mnfltpnf 
 |-  -oo < +oo
2 limsup0 
 |-  ( limsup ` (/) ) = -oo
3 liminf0 
 |-  ( liminf ` (/) ) = +oo
4 2 3 breq12i 
 |-  ( ( limsup ` (/) ) < ( liminf ` (/) ) <-> -oo < +oo )
5 1 4 mpbir 
 |-  ( limsup ` (/) ) < ( liminf ` (/) )