Metamath Proof Explorer


Theorem liminfltlimsupex

Description: An example where the liminf is strictly smaller than the limsup . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis liminfltlimsupex.1 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 2 ∥ 𝑛 , 0 , 1 ) )
Assertion liminfltlimsupex ( lim inf ‘ 𝐹 ) < ( lim sup ‘ 𝐹 )

Proof

Step Hyp Ref Expression
1 liminfltlimsupex.1 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 2 ∥ 𝑛 , 0 , 1 ) )
2 0lt1 0 < 1
3 1 liminf10ex ( lim inf ‘ 𝐹 ) = 0
4 1 limsup10ex ( lim sup ‘ 𝐹 ) = 1
5 3 4 breq12i ( ( lim inf ‘ 𝐹 ) < ( lim sup ‘ 𝐹 ) ↔ 0 < 1 )
6 2 5 mpbir ( lim inf ‘ 𝐹 ) < ( lim sup ‘ 𝐹 )