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

Metamath Proof Explorer

Theorem climliminflimsup4

Description: A sequence of real numbers converges if and only if its superior limit is real and equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		climliminflimsup4.1	\|- ( ph -> M e. ZZ )
2		climliminflimsup4.2	\|- Z = ( ZZ>= ` M )
3		climliminflimsup4.3	\|- ( ph -> F : Z --> RR )
4	1 2 3	climliminflimsup2	\|- ( ph -> ( F e. dom ~~> <-> ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) ) )
5	3	frexr	\|- ( ph -> F : Z --> RR* )
6	1 2 5	liminfgelimsupuz	\|- ( ph -> ( ( limsup ` F ) <_ ( liminf ` F ) <-> ( liminf ` F ) = ( limsup ` F ) ) )
7	6	anbi2d	\|- ( ph -> ( ( ( limsup ` F ) e. RR /\ ( limsup ` F ) <_ ( liminf ` F ) ) <-> ( ( limsup ` F ) e. RR /\ ( liminf ` F ) = ( limsup ` F ) ) ) )
8	4 7	bitrd	\|- ( ph -> ( F e. dom ~~> <-> ( ( limsup ` F ) e. RR /\ ( liminf ` F ) = ( limsup ` F ) ) ) )