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

Metamath Proof Explorer

Theorem liminfgelimsupuz

Proof