Theorem climlimsup

Description: A sequence of real numbers converges if and only if it converges to its superior limit. The first hypothesis is needed (see climlimsupcex for a counterexample). (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		climlimsup.1	|- ( ph -> M e. ZZ )
2		climlimsup.2	|- Z = ( ZZ>= ` M )
3		climlimsup.3	|- ( ph -> F : Z --> RR )
4	3	adantr	|- ( ( ph /\ F e. dom ~~> ) -> F : Z --> RR )
5	1	adantr	|- ( ( ph /\ F e. dom ~~> ) -> M e. ZZ )
6		simpr	|- ( ( ph /\ F e. dom ~~> ) -> F e. dom ~~> )
7	2	climcau	|- ( ( M e. ZZ /\ F e. dom ~~> ) -> A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )
8	5 6 7	syl2anc	|- ( ( ph /\ F e. dom ~~> ) -> A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )
9	2 4 8	caurcvg	|- ( ( ph /\ F e. dom ~~> ) -> F ~~> ( limsup ` F ) )
10		climrel	|- Rel ~~>
11		releldm	|- ( ( Rel ~~> /\ F ~~> ( limsup ` F ) ) -> F e. dom ~~> )
12	10 11	mpan	|- ( F ~~> ( limsup ` F ) -> F e. dom ~~> )
13	12	adantl	|- ( ( ph /\ F ~~> ( limsup ` F ) ) -> F e. dom ~~> )
14	9 13	impbida	|- ( ph -> ( F e. dom ~~> <-> F ~~> ( limsup ` F ) ) )