Metamath Proof Explorer

Theorem climliminflimsup

Description: A sequence of real numbers converges if and only if its inferior limit is real and it is greater than or equal to its superior limit (in such a case, they are actually equal, see liminfgelimsupuz ). (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses climliminflimsup.1 
|- ( ph -> M e. ZZ )
climliminflimsup.2 
|- Z = ( ZZ>= ` M )
climliminflimsup.3 
|- ( ph -> F : Z --> RR )
Assertion climliminflimsup 
|- ( ph -> ( F e. dom ~~> <-> ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 climliminflimsup.1 
 |-  ( ph -> M e. ZZ )
2 climliminflimsup.2 
 |-  Z = ( ZZ>= ` M )
3 climliminflimsup.3 
 |-  ( ph -> F : Z --> RR )
4 1 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> M e. ZZ )
5 1 2 3 climliminf 
 |-  ( ph -> ( F e. dom ~~> <-> F ~~> ( liminf ` F ) ) )
6 5 biimpd 
 |-  ( ph -> ( F e. dom ~~> -> F ~~> ( liminf ` F ) ) )
7 6 imp 
 |-  ( ( ph /\ F e. dom ~~> ) -> F ~~> ( liminf ` F ) )
8 3 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> F : Z --> RR )
9 8 ffvelcdmda 
 |-  ( ( ( ph /\ F e. dom ~~> ) /\ k e. Z ) -> ( F ` k ) e. RR )
10 2 4 7 9 climrecl 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( liminf ` F ) e. RR )
11 simpr 
 |-  ( ( ph /\ F e. dom ~~> ) -> F e. dom ~~> )
12 11 limsupcld 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( limsup ` F ) e. RR* )
13 4 2 8 11 climliminflimsupd 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( liminf ` F ) = ( limsup ` F ) )
14 13 eqcomd 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( limsup ` F ) = ( liminf ` F ) )
15 12 14 xreqled 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( limsup ` F ) <_ ( liminf ` F ) )
16 10 15 jca 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) )
17 1 adantr 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> M e. ZZ )
18 3 adantr 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> F : Z --> RR )
19 simprl 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( liminf ` F ) e. RR )
20 simprr 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( limsup ` F ) <_ ( liminf ` F ) )
21 17 2 18 19 20 liminflimsupclim 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> F e. dom ~~> )
22 16 21 impbida 
 |-  ( ph -> ( F e. dom ~~> <-> ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) )