P. 134 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	absnegd 13301	Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscjd 13302	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` ( * ` A ) ) = ( abs ` A ) )
Theorem	releabsd 13303	The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` A ) <_ ( abs ` A ) )
Theorem	absexpd 13304	Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )
Theorem	abssubd 13305	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
Theorem	absmuld 13306	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
Theorem	absdivd 13307	Absolute value distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )
Theorem	abstrid 13308	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs2difd 13309	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) )
Theorem	abs2dif2d 13310	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs2difabsd 13311	Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) )
Theorem	abs3difd 13312	Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
Theorem	abs3lemd 13313	Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. RR )   &    |- ( ph -> ( abs ` ( A - C ) ) < ( D / 2 ) )   &    |- ( ph -> ( abs ` ( C - B ) ) < ( D / 2 ) )   =>    |- ( ph -> ( abs ` ( A - B ) ) < D )
5.10  Elementary limits and convergence
5.10.1  Superior limit (lim sup)
Syntax	clsp 13314	Extend class notation to include the limsup function.
class limsup
Definition	df-limsup 13315*	Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 13318 for its value. (Contributed by NM, 26-Oct-2005.)
|- limsup = ( x e. _V |-> sup ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , `' < ) )
Theorem	limsupgord 13316	Ordering property of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> sup ( ( ( F " ( B [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) )
Theorem	limsupcl 13317	Closure of the superior limit. (Contributed by NM, 26-Oct-2005.) (Revised by Mario Carneiro, 7-May-2016.)
|- ( F e. V -> ( limsup ` F ) e. RR* )
Theorem	limsupval 13318*	The superior limit of an infinite sequence F of extended real numbers, which is the infimum (indicated by `' <) of the set of suprema of all upper infinite subsequences of F. Definition 12-4.1 of [Gleason] p. 175. (Contributed by NM, 26-Oct-2005.) (Revised by Mario Carneiro, 5-Sep-2014.)
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( F e. V -> ( limsup ` F ) = sup ( ran G , RR* , `' < ) )
Theorem	limsupgf 13319*	Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- G : RR --> RR*
Theorem	limsupgval 13320*	Value of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( M e. RR -> ( G ` M ) = sup ( ( ( F " ( M [,) +oo ) ) i^i RR* ) , RR* , < ) )
Theorem	limsupgle 13321*	The defining property of the superior limit function. (Contributed by Mario Carneiro, 5-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( G ` C ) <_ A <-> A. j e. B ( C <_ j -> ( F ` j ) <_ A ) ) )
Theorem	limsuple 13322*	The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ ( limsup ` F ) <-> A. j e. RR A <_ ( G ` j ) ) )
Theorem	limsuplt 13323*	The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   =>    |- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( ( limsup ` F ) < A <-> E. j e. RR ( G ` j ) < A ) )
Theorem	limsupval2 13324*	The superior limit, relativized to an unbounded set. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 8-May-2016.)
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   &    |- ( ph -> F e. V )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   =>    |- ( ph -> ( limsup ` F ) = sup ( ( G " A ) , RR* , `' < ) )
Theorem	limsupgre 13325*	If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) -> G : RR --> RR )
Theorem	limsupbnd1 13326*	If a sequence is eventually at most A, then the limsup is also at most A. (The converse is only true if the less or equal is replaced by strictly less than; consider the sequence 1 / n which is never less or equal to zero even though the limsup is.) (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
|- ( 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	limsupbnd2 13327*	If a sequence is eventually greater than A, then the limsup is also greater than A. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
|- ( ph -> B C_ RR )   &    |- ( ph -> F : B --> RR* )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> sup ( B , RR* , < ) = +oo )   &    |- ( ph -> E. k e. RR A. j e. B ( k <_ j -> A <_ ( F ` j ) ) )   =>    |- ( ph -> A <_ ( limsup ` F ) )
5.10.2  Limits
Syntax	cli 13328	Extend class notation with convergence relation for limits.
class ~~>
Syntax	crli 13329	Extend class notation with real convergence relation for limits.
class ~~> r
Syntax	co1 13330	Extend class notation with the set of all eventually bounded functions.
class O(1)
Syntax	clo1 13331	Extend class notation with the set of all eventually upper bounded functions.
class <_O(1)
Definition	df-clim 13332*	Define the limit relation for complex number sequences. See clim 13338 for its relational expression. (Contributed by NM, 28-Aug-2005.)
|- ~~> = { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }
Definition	df-rlim 13333*	Define the limit relation for partial functions on the reals. See rlim 13339 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 13334*	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 13335*	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 13336	The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Rel ~~>
Theorem	rlimrel 13337	The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.)
|- Rel ~~> r
Theorem	clim 13338*	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 13339*	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 13340*	Rewrite rlim 13339 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 13341*	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 13342*	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 13343	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 13344	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 13345	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 13346	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 13347	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 13348*	Express the predicate: The limit of complex number sequence F is A, or F converges to A, with more general quantifier restrictions than clim 13338. (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 13349*	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 13350*	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 13351*	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 13352*	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 13353*	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 13354*	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 13355*	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 13356*	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 13357*	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 13358*	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 13359*	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 13360*	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 13361*	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 13362	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 13363	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 13364*	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 13365*	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 13366*	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 13367*	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 13368*	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 13369*	Refine o1bdd2 13385 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 13370*	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 13371*	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 13372*	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 13373	An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( F e. O(1) -> F : dom F --> CC )
Theorem	o1dm 13374	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 13375*	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 13376	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 13377*	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 13378*	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 13379*	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 13380*	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 13381*	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 13382*	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 13383*	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 13384*	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 13385*	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 13386*	Refine o1bdd2 13385 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 13387*	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 13388*	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 13389	Forward direction of rlimclim 13390. (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 13390	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 13391*	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 13392	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 13393	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 13394	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 13395	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 13396	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 13397	The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ~~> : dom ~~> --> CC
Theorem	climdm 13398	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 13399*	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 13400*	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 )