P. 400 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39901-40000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	climfveq 39901*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( ~~> ` F ) = ( ~~> ` G ) )
Theorem	clim2f2 39902*	Express the predicate: The limit of complex number sequence F is A, or F converges to A, with more general quantifier restrictions than clim 14225. Similar to clim2 14235, but without the disjoint var constraint F k. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/ k ph   &    |- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   =>    |- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
Theorem	climfveqmpt 39903*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ k ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. R )   &    |- ( ph -> Z C_ A )   &    |- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> C e. S )   &    |- ( ph -> Z C_ C )   &    |- ( ( ph /\ k e. C ) -> D e. W )   &    |- ( ( ph /\ k e. Z ) -> B = D )   =>    |- ( ph -> ( ~~> ` ( k e. A |-> B ) ) = ( ~~> ` ( k e. C |-> D ) ) )
Theorem	climd 39904*	Express the predicate: The limit of complex number sequence F is A, or F converges to A. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> X e. RR+ )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) )
Theorem	clim2d 39905*	The limit of complex number sequence F is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> X e. RR+ )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) )
Theorem	fnlimfvre 39906*	The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ m ph   &    |- F/_ m F   &    |- F/_ x F   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
Theorem	allbutfifvre 39907*	Given a sequence of real-valued functions, and X that belongs to all but finitely many domains, then its function value is ultimately a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ m ph   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )   &    |- D = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )   &    |- ( ph -> X e. D )   =>    |- ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) e. RR )
Theorem	climleltrp 39908*	The limit of complex number sequence F is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) e. RR )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> X e. RR+ )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) )
Theorem	fnlimfvre2 39909*	The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ m ph   &    |- F/_ m F   &    |- F/_ x F   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }   &    |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( G ` X ) e. RR )
Theorem	fnlimf 39910*	The limit function of real functions, is a real-valued function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ m ph   &    |- F/_ m F   &    |- F/_ x F   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }   &    |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   =>    |- ( ph -> G : D --> RR )
Theorem	fnlimabslt 39911*	A sequence of function values, approximates the corresponding limit function value, all but finitely many times. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ m ph   &    |- F/_ m F   &    |- F/_ x F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }   &    |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. RR+ )   =>    |- ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. RR /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )
Theorem	climfveqf 39912*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k G   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( ~~> ` F ) = ( ~~> ` G ) )
Theorem	climmptf 39913*	Exhibit a function G with the same convergence properties as the not-quite-function F. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ k F   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- Z = ( ZZ>= ` M )   &    |- G = ( k e. Z |-> ( F ` k ) )   =>    |- ( ph -> ( F ~~> A <-> G ~~> A ) )
Theorem	climfveqmpt3 39914*	Two functions that are eventually equal to one another have the same limit. TODO: this is more general than climfveqmpt 39903 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   &    |- ( ph -> Z C_ A )   &    |- ( ph -> Z C_ C )   &    |- ( ( ph /\ k e. Z ) -> B e. U )   &    |- ( ( ph /\ k e. Z ) -> B = D )   =>    |- ( ph -> ( ~~> ` ( k e. A |-> B ) ) = ( ~~> ` ( k e. C |-> D ) ) )
Theorem	climeldmeqf 39915*	Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k G   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( F e. dom ~~> <-> G e. dom ~~> ) )
Theorem	climreclmpt 39916*	The limit of B convergent real sequence is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   &    |- ( ph -> ( k e. Z |-> A ) ~~> B )   =>    |- ( ph -> B e. RR )
Theorem	limsupref 39917*	If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> E. b e. RR E. k e. RR A. j e. A ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )   =>    |- ( ph -> ( limsup ` F ) e. RR )
Theorem	limsupbnd1f 39918*	If a sequence is eventually at most A, then the limsup is also at most A. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> B C_ RR )   &    |- ( ph -> F : B --> RR* )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ A ) )   =>    |- ( ph -> ( limsup ` F ) <_ A )
Theorem	climbddf 39919*	A converging sequence of complex numbers is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ k F   &    |- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x )
Theorem	climeqf 39920*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k G   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( F ~~> A <-> G ~~> A ) )
Theorem	climeldmeqmpt3 39921*	Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt 39900 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   &    |- ( ph -> Z C_ A )   &    |- ( ph -> Z C_ C )   &    |- ( ( ph /\ k e. Z ) -> B e. U )   &    |- ( ( ph /\ k e. Z ) -> B = D )   =>    |- ( ph -> ( ( k e. A |-> B ) e. dom ~~> <-> ( k e. C |-> D ) e. dom ~~> ) )
Theorem	limsupcld 39922	Closure of the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F e. V )   =>    |- ( ph -> ( limsup ` F ) e. RR* )
Theorem	climfv 39923	The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( F ~~> A -> A = ( ~~> ` F ) )
Theorem	limsupval3 39924*	The superior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> RR* )   &    |- G = ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) )   =>    |- ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
Theorem	climfveqmpt2 39925*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> Z C_ A )   &    |- ( ph -> Z C_ B )   &    |- ( ( ph /\ k e. Z ) -> C e. U )   =>    |- ( ph -> ( ~~> ` ( k e. A |-> C ) ) = ( ~~> ` ( k e. B |-> C ) ) )
Theorem	limsup0 39926	The superior limit of the empty set (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( limsup ` (/) ) = -oo
Theorem	climeldmeqmpt2 39927*	Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. W )   &    |- ( ph -> B e. V )   &    |- ( ph -> Z C_ A )   &    |- ( ph -> Z C_ B )   &    |- ( ( ph /\ k e. Z ) -> C e. U )   =>    |- ( ph -> ( ( k e. A |-> C ) e. dom ~~> <-> ( k e. B |-> C ) e. dom ~~> ) )
Theorem	limsupresre 39928	The supremum limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F e. V )   =>    |- ( ph -> ( limsup ` ( F |` RR ) ) = ( limsup ` F ) )
Theorem	climeqmpt 39929*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> Z C_ A )   &    |- ( ph -> Z C_ B )   &    |- ( ( ph /\ x e. Z ) -> C e. U )   =>    |- ( ph -> ( ( x e. A |-> C ) ~~> D <-> ( x e. B |-> C ) ~~> D ) )
Theorem	climfvd 39930	The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F ~~> A )   =>    |- ( ph -> A = ( ~~> ` F ) )
Theorem	limsuplesup 39931	An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F e. V )   &    |- ( ph -> K e. RR )   =>    |- ( ph -> ( limsup ` F ) <_ sup ( ( ( F " ( K [,) +oo ) ) i^i RR* ) , RR* , < ) )
Theorem	limsupresico 39932	The superior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. RR )   &    |- Z = ( M [,) +oo )   &    |- ( ph -> F e. V )   =>    |- ( ph -> ( limsup ` ( F |` Z ) ) = ( limsup ` F ) )
Theorem	limsuppnfdlem 39933*	If the restriction of a function to every upper interval is unbounded above, its limsup is +oo. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   &    |- ( ph -> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )   &    |- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( ph -> ( limsup ` F ) = +oo )
Theorem	limsuppnfd 39934*	If the restriction of a function to every upper interval is unbounded above, its limsup is +oo. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   &    |- ( ph -> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )   =>    |- ( ph -> ( limsup ` F ) = +oo )
Theorem	limsupresuz 39935	If the real part of the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> dom ( F |` RR ) C_ ZZ )   =>    |- ( ph -> ( limsup ` ( F |` Z ) ) = ( limsup ` F ) )
Theorem	limsupub 39936*	If the limsup is not +oo, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   &    |- ( ph -> ( limsup ` F ) =/= +oo )   =>    |- ( ph -> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
Theorem	limsupres 39937	The superior limit of a restriction is less than or equal to the original superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F e. V )   =>    |- ( ph -> ( limsup ` ( F |` C ) ) <_ ( limsup ` F ) )
Theorem	climinf2lem 39938*	A convergent, non-increasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )   =>    |- ( ph -> F ~~> inf ( ran F , RR* , < ) )
Theorem	climinf2 39939*	A convergent, non-increasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )   =>    |- ( ph -> F ~~> inf ( ran F , RR* , < ) )
Theorem	limsupvaluz 39940*	The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -oo and the r.h.s. would be +oo). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR* )   =>    |- ( ph -> ( limsup ` F ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR* , < ) )
Theorem	limsupresuz2 39941	If the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> dom F C_ ZZ )   =>    |- ( ph -> ( limsup ` ( F |` Z ) ) = ( limsup ` F ) )
Theorem	limsuppnflem 39942*	If the restriction of a function to every upper interval is unbounded above, its limsup is +oo. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) = +oo <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
Theorem	limsuppnf 39943*	If the restriction of a function to every upper interval is unbounded above, its limsup is +oo. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) = +oo <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
Theorem	limsupubuzlem 39944*	If the limsup is not +oo, then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- F/_ j X   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> K e. RR )   &    |- ( ph -> A. j e. Z ( K <_ j -> ( F ` j ) <_ Y ) )   &    |- N = if ( (⌈ ` K ) <_ M , M , (⌈ ` K ) )   &    |- W = sup ( ran ( j e. ( M ... N ) |-> ( F ` j ) ) , RR , < )   &    |- X = if ( W <_ Y , Y , W )   =>    |- ( ph -> E. x e. RR A. j e. Z ( F ` j ) <_ x )
Theorem	limsupubuz 39945*	For a real-valued function on a set of upper integers, if the superior limit is not +oo, then the function is bounded above. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ph -> ( limsup ` F ) =/= +oo )   =>    |- ( ph -> E. x e. RR A. j e. Z ( F ` j ) <_ x )
Theorem	climinf2mpt 39946*	A bounded below, monotonic non increasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- F/ j ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ k e. Z ) -> B e. RR )   &    |- ( k = j -> B = C )   &    |- ( ( ph /\ k e. Z /\ j = ( k + 1 ) ) -> C <_ B )   &    |- ( ph -> ( k e. Z |-> B ) e. dom ~~> )   =>    |- ( ph -> ( k e. Z |-> B ) ~~> inf ( ran ( k e. Z |-> B ) , RR* , < ) )
Theorem	climinfmpt 39947*	A bounded below, monotonic non increasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- F/ j ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ k e. Z ) -> B e. RR )   &    |- ( k = j -> B = C )   &    |- ( ( ph /\ k e. Z /\ j = ( k + 1 ) ) -> C <_ B )   &    |- ( ph -> E. x e. RR A. k e. Z x <_ B )   =>    |- ( ph -> ( k e. Z |-> B ) ~~> inf ( ran ( k e. Z |-> B ) , RR* , < ) )
Theorem	climinf3 39948*	A convergent, non-increasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ph -> F e. dom ~~> )   =>    |- ( ph -> F ~~> inf ( ran F , RR* , < ) )
Theorem	limsupvaluzmpt 39949*	The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -oo and the r.h.s. would be +oo). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ j e. Z ) -> B e. RR* )   =>    |- ( ph -> ( limsup ` ( j e. Z |-> B ) ) = inf ( ran ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) , RR* , < ) )
Theorem	limsupequzmpt2 39950*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- F/_ j A   &    |- F/_ j B   &    |- A = ( ZZ>= ` M )   &    |- B = ( ZZ>= ` N )   &    |- ( ph -> K e. A )   &    |- ( ph -> K e. B )   &    |- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. V )   =>    |- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )
Theorem	limsupubuzmpt 39951*	If the limsup is not +oo, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ j e. Z ) -> B e. RR )   &    |- ( ph -> ( limsup ` ( j e. Z |-> B ) ) =/= +oo )   =>    |- ( ph -> E. x e. RR A. j e. Z B <_ x )
Theorem	limsupmnflem 39952*	The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   &    |- G = ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) )   =>    |- ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
Theorem	limsupmnf 39953*	The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
Theorem	limsupequzlem 39954*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F Fn ( ZZ>= ` M ) )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> G Fn ( ZZ>= ` N ) )   &    |- ( ph -> K e. ZZ )   &    |- ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( limsup ` F ) = ( limsup ` G ) )
Theorem	limsupequz 39955*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k G   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F Fn ( ZZ>= ` M ) )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> G Fn ( ZZ>= ` N ) )   &    |- ( ph -> K e. ZZ )   &    |- ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( limsup ` F ) = ( limsup ` G ) )
Theorem	limsupre2lem 39956*	Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) ) ) )
Theorem	limsupre2 39957*	Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) ) ) )
Theorem	limsupmnfuzlem 39958*	The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
Theorem	limsupmnfuz 39959*	The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
Theorem	limsupequzmptlem 39960*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- A = ( ZZ>= ` M )   &    |- B = ( ZZ>= ` N )   &    |- ( ( ph /\ j e. A ) -> C e. V )   &    |- ( ( ph /\ j e. B ) -> C e. W )   &    |- K = if ( M <_ N , N , M )   =>    |- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )
Theorem	limsupequzmpt 39961*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- A = ( ZZ>= ` M )   &    |- B = ( ZZ>= ` N )   &    |- ( ( ph /\ j e. A ) -> C e. V )   &    |- ( ( ph /\ j e. B ) -> C e. W )   =>    |- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )
Theorem	limsupre2mpt 39962*	Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   =>    |- ( ph -> ( ( limsup ` ( x e. A |-> B ) ) e. RR <-> ( E. y e. RR A. k e. RR E. x e. A ( k <_ x /\ y < B ) /\ E. y e. RR E. k e. RR A. x e. A ( k <_ x -> B < y ) ) ) )
Theorem	limsupequzmptf 39963*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- F/_ j A   &    |- F/_ j B   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- A = ( ZZ>= ` M )   &    |- B = ( ZZ>= ` N )   &    |- ( ( ph /\ j e. A ) -> C e. V )   &    |- ( ( ph /\ j e. B ) -> C e. W )   =>    |- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )
Theorem	limsupre3lem 39964*	Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller or equal than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger or equal than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) ) )
Theorem	limsupre3 39965*	Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller or equal than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger or equal than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) ) )
Theorem	limsupre3mpt 39966*	Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller or equal than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger or equal than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   =>    |- ( ph -> ( ( limsup ` ( x e. A |-> B ) ) e. RR <-> ( E. y e. RR A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) /\ E. y e. RR E. k e. RR A. x e. A ( k <_ x -> B <_ y ) ) ) )
Theorem	limsupre3uzlem 39967*	Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller or equal than the function, infinitely often; 2. there is a real number that is eventually larger or equal than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )
Theorem	limsupre3uz 39968*	Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller or equal than the function, infinitely often; 2. there is a real number that is eventually larger or equal than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR* )   =>    |- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )
Theorem	limsupreuz 39969*	Given a function on the reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller or equal than the function, infinitely often; 2. there is a real number that is larger or equal than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ j F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   =>    |- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR A. j e. Z ( F ` j ) <_ x ) ) )
Theorem	limsupvaluz2 39970*	The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ph -> ( limsup ` F ) e. RR )   =>    |- ( ph -> ( limsup ` F ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR , < ) )
Theorem	limsupreuzmpt 39971*	Given a function on the reals, defined on a set of upper integers, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller or equal than the function, infinitely often; 2. there is a real number that is larger or equal than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ j e. Z ) -> B e. RR )   =>    |- ( ph -> ( ( limsup ` ( j e. Z |-> B ) ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B /\ E. x e. RR A. j e. Z B <_ x ) ) )
Theorem	supcnvlimsup 39972*	If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ph -> ( limsup ` F ) e. RR )   =>    |- ( ph -> ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) ~~> ( limsup ` F ) )
Theorem	supcnvlimsupmpt 39973*	If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ j e. Z ) -> B e. RR )   &    |- ( ph -> ( limsup ` ( j e. Z |-> B ) ) e. RR )   =>    |- ( ph -> ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) ~~> ( limsup ` ( j e. Z |-> B ) ) )
Theorem	0cnv 39974	If (/) is a complex number, then it converges to itself. (see 0ncn 9954 and its comment ; see also the comment in climlimsupcex 40001) (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( (/) e. CC -> (/) ~~> (/) )
Theorem	climuzlem 39975*	Express the predicate: The limit of complex number sequence F is A, or F converges to A. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> CC )   =>    |- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
Theorem	climuz 39976*	Express the predicate: The limit of complex number sequence F is A, or F converges to A. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/_ k F   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> CC )   =>    |- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
Theorem	lmbr3v 39977*	Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> J e. (TopOn ` X ) )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
Theorem	climisp 39978*	If a sequence converges to an isolated point (w.r.t. the standard topology on the complex numbers) then the sequence eventually becomes that point. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> CC )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> X e. RR+ )   &    |- ( ( ph /\ k e. Z /\ ( F ` k ) =/= A ) -> X <_ ( abs ` ( ( F ` k ) - A ) ) )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) = A )
Theorem	lmbr3 39979*	Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- F/_ k F   &    |- ( ph -> J e. (TopOn ` X ) )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
Theorem	climrescn 39980*	A sequence converging w.r.t. the standard topology on the complex numbers, eventually becomes a sequence of complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F Fn Z )   &    |- ( ph -> F e. dom ~~> )   =>    |- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC )
Theorem	climxrrelem 39981*	If a seqence ranging over the extended reals converges w.r.t. the standard topology on the complex numbers, then there exists an upper set of the integers over which the function is real-valued. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR* )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> D e. RR+ )   &    |- ( ( ph /\ +oo e. CC ) -> D <_ ( abs ` ( +oo - A ) ) )   &    |- ( ( ph /\ -oo e. CC ) -> D <_ ( abs ` ( -oo - A ) ) )   =>    |- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
Theorem	climxrre 39982*	If a sequence ranging over the extended reals converges w.r.t. the standard topology on the complex numbers, then there exists an upper set of the integers over which the function is real-valued (the weaker hypothesis F e. dom ~~> is probably not enough, since in principle we could have +oo e. CC and -oo e. CC). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR* )   &    |- ( ph -> A e. RR )   &    |- ( ph -> F ~~> A )   =>    |- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
20.32.7.1  Inferior limit (lim inf)
Syntax	clsi 39983	Extend class notation to include the liminf function. (actually, it makes sense for any extended real function defined on a subset of RR which is not upper-bounded)
class liminf
Definition	df-liminf 39984*	Define the inferior limit of a sequence of extended real numbers. (Contributed by GS, 2-Jan-2022.)
|- liminf = ( x e. _V |-> sup ( ran ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
Theorem	limsuplt2 39985*	The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> B C_ RR )   &    |- ( ph -> F : B --> RR* )   &    |- ( ph -> A e. RR* )   =>    |- ( ph -> ( ( limsup ` F ) < A <-> E. k e. RR sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) < A ) )
Theorem	liminfgord 39986	Ordering property of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> inf ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ( ( F " ( B [,) +oo ) ) i^i RR* ) , RR* , < ) )
Theorem	limsupvald 39987*	The superior limit of a sequence F of extended real numbers is the infimum of the set of suprema of all restrictions of F to an upperset of reals . (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> F e. V )   &    |- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
Theorem	limsupresicompt 39988*	The superior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. V )   &    |- ( ph -> M e. RR )   &    |- Z = ( M [,) +oo )   =>    |- ( ph -> ( limsup ` ( x e. A |-> B ) ) = ( limsup ` ( x e. ( A i^i Z ) |-> B ) ) )
Theorem	limsupcli 39989	Closure of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F e. V   =>    |- ( limsup ` F ) e. RR*
Theorem	liminfgf 39990	Closure of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- G : RR --> RR*
Theorem	liminfval 39991*	The inferior limit of a set F. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( F e. V -> (liminf ` F ) = sup ( ran G , RR* , < ) )
Theorem	climlimsup 39992	A sequence of real numbers converges if and only if it converges to its superior limit. The first hypothesis is needed (see climlimsupcex 40001 for a counterexample) (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   =>    |- ( ph -> ( F e. dom ~~> <-> F ~~> ( limsup ` F ) ) )
Theorem	limsupge 39993*	The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> B C_ RR )   &    |- ( ph -> F : B --> RR* )   &    |- ( ph -> A e. RR* )   =>    |- ( ph -> ( A <_ ( limsup ` F ) <-> A. k e. RR A <_ sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
Theorem	liminfgval 39994*	Value of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( M e. RR -> ( G ` M ) = inf ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) )
Theorem	liminfcl 39995	Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( F e. V -> (liminf ` F ) e. RR* )
Theorem	liminfvald 39996*	The inferior limit of a set F. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> F e. V )   &    |- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( ph -> (liminf ` F ) = sup ( ran G , RR* , < ) )
Theorem	liminfval5 39997*	The inferior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> RR* )   &    |- G = ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) )   =>    |- ( ph -> (liminf ` F ) = sup ( ran G , RR* , < ) )
Theorem	limsupresxr 39998	The superior limit of a function only depends on the restriction of that function to the preimage of the set of extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> F e. V )   &    |- ( ph -> Fun F )   &    |- A = ( `' F " RR* )   =>    |- ( ph -> ( limsup ` ( F |` A ) ) = ( limsup ` F ) )
Theorem	liminfresxr 39999	The inferior limit of a function only depends on the preimage of the extended real part. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> F e. V )   &    |- ( ph -> Fun F )   &    |- A = ( `' F " RR* )   =>    |- ( ph -> (liminf ` ( F |` A ) ) = (liminf ` F ) )
Theorem	liminfval2 40000*	The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   &    |- ( ph -> F e. V )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   =>    |- ( ph -> (liminf ` F ) = sup ( ( G " A ) , RR* , < ) )