Metamath Proof Explorer


Theorem liminfgelimsupuz

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 liminfgelimsupuz.1
|- ( ph -> M e. ZZ )
liminfgelimsupuz.2
|- Z = ( ZZ>= ` M )
liminfgelimsupuz.3
|- ( ph -> F : Z --> RR* )
Assertion liminfgelimsupuz
|- ( ph -> ( ( limsup ` F ) <_ ( liminf ` F ) <-> ( liminf ` F ) = ( limsup ` F ) ) )

Proof

Step Hyp Ref Expression
1 liminfgelimsupuz.1
 |-  ( ph -> M e. ZZ )
2 liminfgelimsupuz.2
 |-  Z = ( ZZ>= ` M )
3 liminfgelimsupuz.3
 |-  ( ph -> F : Z --> RR* )
4 2 fvexi
 |-  Z e. _V
5 4 a1i
 |-  ( ph -> Z e. _V )
6 3 5 fexd
 |-  ( ph -> F e. _V )
7 6 liminfcld
 |-  ( ph -> ( liminf ` F ) e. RR* )
8 7 adantr
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) e. RR* )
9 6 limsupcld
 |-  ( ph -> ( limsup ` F ) e. RR* )
10 9 adantr
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( limsup ` F ) e. RR* )
11 1 2 3 liminflelimsupuz
 |-  ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )
12 11 adantr
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) <_ ( limsup ` F ) )
13 simpr
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( limsup ` F ) <_ ( liminf ` F ) )
14 8 10 12 13 xrletrid
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) = ( limsup ` F ) )
15 9 adantr
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) e. RR* )
16 id
 |-  ( ( liminf ` F ) = ( limsup ` F ) -> ( liminf ` F ) = ( limsup ` F ) )
17 16 eqcomd
 |-  ( ( liminf ` F ) = ( limsup ` F ) -> ( limsup ` F ) = ( liminf ` F ) )
18 17 adantl
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) = ( liminf ` F ) )
19 15 18 xreqled
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) <_ ( liminf ` F ) )
20 14 19 impbida
 |-  ( ph -> ( ( limsup ` F ) <_ ( liminf ` F ) <-> ( liminf ` F ) = ( limsup ` F ) ) )