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

Metamath Proof Explorer

Theorem liminfgelimsup

Description: The inferior limit is greater than or equal to the superior limit if and only if they are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfgelimsup.1 
|- ( ph -> F e. V )
liminfgelimsup.2 
|- ( ph -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
Assertion liminfgelimsup 
|- ( ph -> ( ( limsup ` F ) <_ ( liminf ` F ) <-> ( liminf ` F ) = ( limsup ` F ) ) )

Proof

Step Hyp Ref Expression
1 liminfgelimsup.1 
 |-  ( ph -> F e. V )
2 liminfgelimsup.2 
 |-  ( ph -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
3 1 liminfcld 
 |-  ( ph -> ( liminf ` F ) e. RR* )
4 3 adantr 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) e. RR* )
5 1 limsupcld 
 |-  ( ph -> ( limsup ` F ) e. RR* )
6 5 adantr 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( limsup ` F ) e. RR* )
7 1 2 liminflelimsup 
 |-  ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )
8 7 adantr 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) <_ ( limsup ` F ) )
9 simpr 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( limsup ` F ) <_ ( liminf ` F ) )
10 4 6 8 9 xrletrid 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) = ( limsup ` F ) )
11 5 adantr 
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) e. RR* )
12 id 
 |-  ( ( liminf ` F ) = ( limsup ` F ) -> ( liminf ` F ) = ( limsup ` F ) )
13 12 eqcomd 
 |-  ( ( liminf ` F ) = ( limsup ` F ) -> ( limsup ` F ) = ( liminf ` F ) )
14 13 adantl 
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) = ( liminf ` F ) )
15 11 14 xreqled 
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) <_ ( liminf ` F ) )
16 10 15 impbida 
 |-  ( ph -> ( ( limsup ` F ) <_ ( liminf ` F ) <-> ( liminf ` F ) = ( limsup ` F ) ) )