P. 137 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13601-13700   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-rlim 13601*	Define the limit relation for partial functions on the reals. See rlim 13607 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ~~> r = { <. f , x >. | ( ( f e. ( CC ^pm RR ) /\ x e. CC ) /\ A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y ) ) }
Definition	df-o1 13602*	Define the set of eventually bounded functions. We don't bother to build the full conception of big-O notation, because we can represent any big-O in terms of O(1) and division, and any little-O in terms of a limit and division. We could also use limsup for this, but it only works on integer sequences, while this will work for real sequences or integer sequences. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- O(1) = { f e. ( CC ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( abs ` ( f ` y ) ) <_ m }
Definition	df-lo1 13603*	Define the set of eventually upper bounded real functions. This fills a gap in O(1) coverage, to express statements like f ( x ) <_ g ( x ) + O ( x ) via ( x e. RR+ |-> ( f ( x ) - g ( x ) ) / x ) e. <_O(1). (Contributed by Mario Carneiro, 25-May-2016.)
|- <_O(1) = { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m }
Theorem	climrel 13604	The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Rel ~~>
Theorem	rlimrel 13605	The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.)
|- Rel ~~> r
Theorem	clim 13606*	Express the predicate: The limit of complex number sequence F is A, or F converges to A. This means that for any real x, no matter how small, there always exists an integer j such that the absolute difference of any later complex number in the sequence and the limit is less than x. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ph -> F e. V )   &    |- ( ( ph /\ k e. ZZ ) -> ( F ` k ) = B )   =>    |- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
Theorem	rlim 13607*	Express the predicate: The limit of complex number function F is C, or F converges to C, in the real sense. This means that for any real x, no matter how small, there always exists a number y such that the absolute difference of any number in the function beyond y and the limit is less than x. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ RR )   &    |- ( ( ph /\ z e. A ) -> ( F ` z ) = B )   =>    |- ( ph -> ( F ~~> r C <-> ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) )
Theorem	rlim2 13608*	Rewrite rlim 13607 for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.)
|- ( ph -> A. z e. A B e. CC )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( z e. A |-> B ) ~~> r C <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
Theorem	rlim2lt 13609*	Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( ph -> A. z e. A B e. CC )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( z e. A |-> B ) ~~> r C <-> A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) )
Theorem	rlim3 13610*	Restrict the range of the domain bound to reals greater than some D e. RR. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( ph -> A. z e. A B e. CC )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. RR )   =>    |- ( ph -> ( ( z e. A |-> B ) ~~> r C <-> A. x e. RR+ E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
Theorem	climcl 13611	Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( F ~~> A -> A e. CC )
Theorem	rlimpm 13612	Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( F ~~> r A -> F e. ( CC ^pm RR ) )
Theorem	rlimf 13613	Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( F ~~> r A -> F : dom F --> CC )
Theorem	rlimss 13614	Domain closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( F ~~> r A -> dom F C_ RR )
Theorem	rlimcl 13615	Closure of the limit of a sequence of complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( F ~~> r A -> A e. CC )
Theorem	clim2 13616*	Express the predicate: The limit of complex number sequence F is A, or F converges to A, with more general quantifier restrictions than clim 13606. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- 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	clim2c 13617*	Express the predicate F converges to A. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> ( F ~~> A <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x ) )
Theorem	clim0 13618*	Express the predicate F converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   =>    |- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) ) )
Theorem	clim0c 13619*	Express the predicate F converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
Theorem	rlim0 13620*	Express the predicate B ( z ) converges to 0. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.)
|- ( ph -> A. z e. A B e. CC )   &    |- ( ph -> A C_ RR )   =>    |- ( ph -> ( ( z e. A |-> B ) ~~> r 0 <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` B ) < x ) ) )
Theorem	rlim0lt 13621*	Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.)
|- ( ph -> A. z e. A B e. CC )   &    |- ( ph -> A C_ RR )   =>    |- ( ph -> ( ( z e. A |-> B ) ~~> r 0 <-> A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` B ) < x ) ) )
Theorem	climi 13622*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. RR+ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> F ~~> A )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < C ) )
Theorem	climi2 13623*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. RR+ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> F ~~> A )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < C )
Theorem	climi0 13624*	Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. RR+ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> F ~~> 0 )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < C )
Theorem	rlimi 13625*	Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015.)
|- ( ph -> A. z e. A B e. V )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> ( z e. A |-> B ) ~~> r C )   =>    |- ( ph -> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) )
Theorem	rlimi2 13626*	Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( ph -> A. z e. A B e. V )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> ( z e. A |-> B ) ~~> r C )   &    |- ( ph -> D e. RR )   =>    |- ( ph -> E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) )
Theorem	ello1 13627*	Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( F e. <_O(1) <-> ( F e. ( RR ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ m ) )
Theorem	ello12 13628*	Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( F : A --> RR /\ A C_ RR ) -> ( F e. <_O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( F ` y ) <_ m ) ) )
Theorem	ello12r 13629*	Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ( F : A --> RR /\ A C_ RR ) /\ ( C e. RR /\ M e. RR ) /\ A. x e. A ( C <_ x -> ( F ` x ) <_ M ) ) -> F e. <_O(1) )
Theorem	lo1f 13630	An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( F e. <_O(1) -> F : dom F --> RR )
Theorem	lo1dm 13631	An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( F e. <_O(1) -> dom F C_ RR )
Theorem	lo1bdd 13632*	The defining property of an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( F e. <_O(1) /\ F : A --> RR ) -> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( F ` y ) <_ m ) )
Theorem	ello1mpt 13633*	Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> B <_ m ) ) )
Theorem	ello1mpt2 13634*	Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> E. y e. ( C [,) +oo ) E. m e. RR A. x e. A ( y <_ x -> B <_ m ) ) )
Theorem	ello1d 13635*	Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> M e. RR )   &    |- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B <_ M )   =>    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )
Theorem	lo1bdd2 13636*	If an eventually bounded function is bounded on every interval A i^i ( -oo , y ) by a function M ( y ), then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )   &    |- ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> B <_ M )   =>    |- ( ph -> E. m e. RR A. x e. A B <_ m )
Theorem	lo1bddrp 13637*	Refine o1bdd2 13653 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )   &    |- ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> B <_ M )   =>    |- ( ph -> E. m e. RR+ A. x e. A B <_ m )
Theorem	elo1 13638*	Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( F e. O(1) <-> ( F e. ( CC ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m ) )
Theorem	elo12 13639*	Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
Theorem	elo12r 13640*	Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( ( F : A --> CC /\ A C_ RR ) /\ ( C e. RR /\ M e. RR ) /\ A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) -> F e. O(1) )
Theorem	o1f 13641	An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( F e. O(1) -> F : dom F --> CC )
Theorem	o1dm 13642	An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( F e. O(1) -> dom F C_ RR )
Theorem	o1bdd 13643*	The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( F e. O(1) /\ F : A --> CC ) -> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) )
Theorem	lo1o1 13644	A function is eventually bounded iff its absolute value is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( F : A --> CC -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) )
Theorem	lo1o12 13645*	A function is eventually bounded iff its absolute value is eventually upper bounded. (This function is useful for converting theorems about <_O(1) to O(1).) (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) )
Theorem	elo1mpt 13646*	Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 21-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> ( abs ` B ) <_ m ) ) )
Theorem	elo1mpt2 13647*	Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 12-May-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> E. y e. ( C [,) +oo ) E. m e. RR A. x e. A ( y <_ x -> ( abs ` B ) <_ m ) ) )
Theorem	elo1d 13648*	Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 21-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ph -> C e. RR )   &    |- ( ph -> M e. RR )   &    |- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> ( abs ` B ) <_ M )   =>    |- ( ph -> ( x e. A |-> B ) e. O(1) )
Theorem	o1lo1 13649*	A real function is eventually bounded iff it is eventually lower bounded and eventually upper bounded. (Contributed by Mario Carneiro, 25-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) )
Theorem	o1lo12 13650*	A lower bounded real function is eventually bounded iff it is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> M e. RR )   &    |- ( ( ph /\ x e. A ) -> M <_ B )   =>    |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> B ) e. <_O(1) ) )
Theorem	o1lo1d 13651*	A real eventually bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )
Theorem	icco1 13652*	Derive eventual boundedness from separate upper and lower eventual bounds. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( ph -> A C_ RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> M e. RR )   &    |- ( ph -> N e. RR )   &    |- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B e. ( M [,] N ) )   =>    |- ( ph -> ( x e. A |-> B ) e. O(1) )
Theorem	o1bdd2 13653*	If an eventually bounded function is bounded on every interval A i^i ( -oo , y ) by a function M ( y ), then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )   &    |- ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> ( abs ` B ) <_ M )   =>    |- ( ph -> E. m e. RR A. x e. A ( abs ` B ) <_ m )
Theorem	o1bddrp 13654*	Refine o1bdd2 13653 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )   &    |- ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> ( abs ` B ) <_ M )   =>    |- ( ph -> E. m e. RR+ A. x e. A ( abs ` B ) <_ m )
Theorem	climconst 13655*	An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ph -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   =>    |- ( ph -> F ~~> A )
Theorem	rlimconst 13656*	A constant sequence converges to its value. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( ( A C_ RR /\ B e. CC ) -> ( x e. A |-> B ) ~~> r B )
Theorem	rlimclim1 13657	Forward direction of rlimclim 13658. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> r A )   &    |- ( ph -> Z C_ dom F )   =>    |- ( ph -> F ~~> A )
Theorem	rlimclim 13658	A sequence on an upper integer set converges in the real sense iff it converges in the integer sense. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> CC )   =>    |- ( ph -> ( F ~~> r A <-> F ~~> A ) )
Theorem	climrlim2 13659*	Produce a real limit from an integer limit, where the real function is only dependent on the integer part of x. (Contributed by Mario Carneiro, 2-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( n = ( |_ ` x ) -> B = C )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> ( n e. Z |-> B ) ~~> D )   &    |- ( ( ph /\ n e. Z ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> M <_ x )   =>    |- ( ph -> ( x e. A |-> C ) ~~> r D )
Theorem	climconst2 13660	A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- ( ZZ>= ` M ) C_ Z   &    |- Z e. _V   =>    |- ( ( A e. CC /\ M e. ZZ ) -> ( Z X. { A } ) ~~> A )
Theorem	climz 13661	The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- ( ZZ X. { 0 } ) ~~> 0
Theorem	rlimuni 13662	A real function whose domain is unbounded above converges to at most one limit. (Contributed by Mario Carneiro, 8-May-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> F ~~> r B )   &    |- ( ph -> F ~~> r C )   =>    |- ( ph -> B = C )
Theorem	rlimdm 13663	Two ways to express that a function has a limit. (The expression ( ~~> r ` F ) is sometimes useful as a shorthand for "the unique limit of the function F"). (Contributed by Mario Carneiro, 8-May-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   =>    |- ( ph -> ( F e. dom ~~> r <-> F ~~> r ( ~~> r ` F ) ) )
Theorem	climuni 13664	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|- ( ( F ~~> A /\ F ~~> B ) -> A = B )
Theorem	fclim 13665	The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ~~> : dom ~~> --> CC
Theorem	climdm 13666	Two ways to express that a function has a limit. (The expression ( ~~> ` F ) is sometimes useful as a shorthand for "the unique limit of the function F"). (Contributed by Mario Carneiro, 18-Mar-2014.)
|- ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) )
Theorem	climeu 13667*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
|- ( F ~~> A -> E! x F ~~> x )
Theorem	climreu 13668*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
|- ( F ~~> A -> E! x e. CC F ~~> x )
Theorem	climmo 13669*	An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)
|- E* x F ~~> x
Theorem	rlimres 13670	The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( F ~~> r A -> ( F |` B ) ~~> r A )
Theorem	lo1res 13671	The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( F e. <_O(1) -> ( F |` A ) e. <_O(1) )
Theorem	o1res 13672	The restriction of an eventually bounded function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( F e. O(1) -> ( F |` A ) e. O(1) )
Theorem	rlimres2 13673*	The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( ph -> A C_ B )   &    |- ( ph -> ( x e. B |-> C ) ~~> r D )   =>    |- ( ph -> ( x e. A |-> C ) ~~> r D )
Theorem	lo1res2 13674*	The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ph -> A C_ B )   &    |- ( ph -> ( x e. B |-> C ) e. <_O(1) )   =>    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )
Theorem	o1res2 13675*	The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( ph -> A C_ B )   &    |- ( ph -> ( x e. B |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> C ) e. O(1) )
Theorem	lo1resb 13676	The restriction of a function to an unbounded-above interval is eventually upper bounded iff the original is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ph -> F : A --> RR )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( F e. <_O(1) <-> ( F |` ( B [,) +oo ) ) e. <_O(1) ) )
Theorem	rlimresb 13677	The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( F ~~> r C <-> ( F |` ( B [,) +oo ) ) ~~> r C ) )
Theorem	o1resb 13678	The restriction of a function to an unbounded-above interval is eventually bounded iff the original is eventually bounded. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( F e. O(1) <-> ( F |` ( B [,) +oo ) ) e. O(1) ) )
Theorem	climeq 13679*	Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- 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 ~~> A <-> G ~~> A ) )
Theorem	lo1eq 13680*	Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ( ph /\ ( x e. A /\ D <_ x ) ) -> B = C )   =>    |- ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> ( x e. A |-> C ) e. <_O(1) ) )
Theorem	rlimeq 13681*	Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ph -> D e. RR )   &    |- ( ( ph /\ ( x e. A /\ D <_ x ) ) -> B = C )   =>    |- ( ph -> ( ( x e. A |-> B ) ~~> r E <-> ( x e. A |-> C ) ~~> r E ) )
Theorem	o1eq 13682*	Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ph -> D e. RR )   &    |- ( ( ph /\ ( x e. A /\ D <_ x ) ) -> B = C )   =>    |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> C ) e. O(1) ) )
Theorem	climmpt 13683*	Exhibit a function G with the same convergence properties as the not-quite-function F. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- G = ( k e. Z |-> ( F ` k ) )   =>    |- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) )
Theorem	2clim 13684*	If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G e. V )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < x )   &    |- ( ph -> F ~~> A )   =>    |- ( ph -> G ~~> A )
Theorem	climmpt2 13685*	Relate an integer limit on a not-quite-function to a real limit. (Contributed by Mario Carneiro, 17-Sep-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> ( F ~~> A <-> ( n e. Z |-> ( F ` n ) ) ~~> r A ) )
Theorem	climshftlem 13686	A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( M e. ZZ -> ( F ~~> A -> ( F shift M ) ~~> A ) )
Theorem	climres 13687	A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- ( ( M e. ZZ /\ F e. V ) -> ( ( F |` ( ZZ>= ` M ) ) ~~> A <-> F ~~> A ) )
Theorem	climshft 13688	A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- ( ( M e. ZZ /\ F e. V ) -> ( ( F shift M ) ~~> A <-> F ~~> A ) )
Theorem	serclim0 13689	The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|- ( M e. ZZ -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )
Theorem	rlimcld2 13690*	If D is a closed set in the topology of the complex numbers (stated here in basic form), and all the elements of the sequence lie in D, then the limit of the sequence also lies in D. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> ( x e. A |-> B ) ~~> r C )   &    |- ( ph -> D C_ CC )   &    |- ( ( ph /\ y e. ( CC \ D ) ) -> R e. RR+ )   &    |- ( ( ( ph /\ y e. ( CC \ D ) ) /\ z e. D ) -> R <_ ( abs ` ( z - y ) ) )   &    |- ( ( ph /\ x e. A ) -> B e. D )   =>    |- ( ph -> C e. D )
Theorem	rlimrege0 13691*	The limit of a sequence of complex numbers with nonnegative real part has nonnegative real part. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> ( x e. A |-> B ) ~~> r C )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> 0 <_ ( Re ` B ) )   =>    |- ( ph -> 0 <_ ( Re ` C ) )
Theorem	rlimrecl 13692*	The limit of a real sequence is real. (Contributed by Mario Carneiro, 9-May-2016.)
|- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> ( x e. A |-> B ) ~~> r C )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> C e. RR )
Theorem	rlimge0 13693*	The limit of a sequence of nonnegative reals is nonnegative. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> ( x e. A |-> B ) ~~> r C )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> 0 <_ C )
Theorem	climshft2 13694*	A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> F e. W )   &    |- ( ph -> G e. X )   &    |- ( ( ph /\ k e. Z ) -> ( G ` ( k + K ) ) = ( F ` k ) )   =>    |- ( ph -> ( F ~~> A <-> G ~~> A ) )
Theorem	climrecl 13695*	The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.) (Proof shortened by Mario Carneiro, 10-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   =>    |- ( ph -> A e. RR )
Theorem	climge0 13696*	A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.) (Proof shortened by Mario Carneiro, 10-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )   =>    |- ( ph -> 0 <_ A )
Theorem	climabs0 13697*	Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> ( F ~~> 0 <-> G ~~> 0 ) )
Theorem	o1co 13698*	Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> F e. O(1) )   &    |- ( ph -> G : B --> A )   &    |- ( ph -> B C_ RR )   &    |- ( ( ph /\ m e. RR ) -> E. x e. RR A. y e. B ( x <_ y -> m <_ ( G ` y ) ) )   =>    |- ( ph -> ( F o. G ) e. O(1) )
Theorem	o1compt 13699*	Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> F e. O(1) )   &    |- ( ( ph /\ y e. B ) -> C e. A )   &    |- ( ph -> B C_ RR )   &    |- ( ( ph /\ m e. RR ) -> E. x e. RR A. y e. B ( x <_ y -> m <_ C ) )   =>    |- ( ph -> ( F o. ( y e. B |-> C ) ) e. O(1) )
Theorem	rlimcn1 13700*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.)
|- ( ph -> G : A --> X )   &    |- ( ph -> C e. X )   &    |- ( ph -> G ~~> r C )   &    |- ( ph -> F : X --> CC )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) )   =>    |- ( ph -> ( F o. G ) ~~> r ( F ` C ) )