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