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 ) ) ) )