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