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

Metamath Proof Explorer

Theorem climliminflimsup2

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

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

Proof

Step Hyp Ref Expression
1 climliminflimsup2.1 
 |-  ( ph -> M e. ZZ )
2 climliminflimsup2.2 
 |-  Z = ( ZZ>= ` M )
3 climliminflimsup2.3 
 |-  ( ph -> F : Z --> RR )
4 1 2 3 climliminflimsup 
 |-  ( ph -> ( F e. dom ~~> <-> ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) )
5 1 adantr 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> M e. ZZ )
6 3 adantr 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> F : Z --> RR )
7 simprl 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( liminf ` F ) e. RR )
8 simprr 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( limsup ` F ) <_ ( liminf ` F ) )
9 5 2 6 7 8 liminflimsupclim 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> F e. dom ~~> )
10 1 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> M e. ZZ )
11 3 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> F : Z --> RR )
12 simpr 
 |-  ( ( ph /\ F e. dom ~~> ) -> F e. dom ~~> )
13 10 2 11 12 climliminflimsupd 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( liminf ` F ) = ( limsup ` F ) )
14 13 eqcomd 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( limsup ` F ) = ( liminf ` F ) )
15 9 14 syldan 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( limsup ` F ) = ( liminf ` F ) )
16 15 7 eqeltrd 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( limsup ` F ) e. RR )
17 16 8 jca 
 |-  ( ( ph /\ ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) )
18 simpr 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( limsup ` F ) <_ ( liminf ` F ) )
19 1 adantr 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> M e. ZZ )
20 3 frexr 
 |-  ( ph -> F : Z --> RR* )
21 20 adantr 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> F : Z --> RR* )
22 19 2 21 liminfgelimsupuz 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( ( limsup ` F ) <_ ( liminf ` F ) <-> ( liminf ` F ) = ( limsup ` F ) ) )
23 18 22 mpbid 
 |-  ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) = ( limsup ` F ) )
24 23 adantrl 
 |-  ( ( ph /\ ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( liminf ` F ) = ( limsup ` F ) )
25 simprl 
 |-  ( ( ph /\ ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( limsup ` F ) e. RR )
26 24 25 eqeltrd 
 |-  ( ( ph /\ ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( liminf ` F ) e. RR )
27 simprr 
 |-  ( ( ph /\ ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( limsup ` F ) <_ ( liminf ` F ) )
28 26 27 jca 
 |-  ( ( ph /\ ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) -> ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) )
29 17 28 impbida 
 |-  ( ph -> ( ( ( liminf ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) <-> ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) )
30 4 29 bitrd 
 |-  ( ph -> ( F e. dom ~~> <-> ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) )