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

Metamath Proof Explorer

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