P. 133 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sqrmsqd 13201	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrsqd 13202	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqrge0d 13203	The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> 0 <_ ( sqr ` A ) )
Theorem	sqrnegd 13204	The square root of a negative number. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` -u A ) = ( _i x. ( sqr ` A ) ) )
Theorem	absidd 13205	A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( abs ` A ) = A )
Theorem	sqrdivd 13206	Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) )
Theorem	sqrmuld 13207	Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) )
Theorem	sqrsq2d 13208	Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) )
Theorem	sqrled 13209	Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) )
Theorem	sqrltd 13210	Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) )
Theorem	sqr11d 13211	The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> ( sqr ` A ) = ( sqr ` B ) )   =>    |- ( ph -> A = B )
Theorem	absltd 13212	Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) ) )
Theorem	absled 13213	Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) )
Theorem	abssubge0d 13214	Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( abs ` ( B - A ) ) = ( B - A ) )
Theorem	abssuble0d 13215	Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( abs ` ( A - B ) ) = ( B - A ) )
Theorem	absdifltd 13216	The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( abs ` ( A - B ) ) < C <-> ( ( B - C ) < A /\ A < ( B + C ) ) ) )
Theorem	absdifled 13217	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( abs ` ( A - B ) ) <_ C <-> ( ( B - C ) <_ A /\ A <_ ( B + C ) ) ) )
Theorem	abscld 13218	Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) e. RR )
Theorem	sqrcld 13219	Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( sqr ` A ) e. CC )
Theorem	sqrrege0d 13220	The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( Re ` ( sqr ` A ) ) )
Theorem	sqsqrd 13221	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	msqsqrd 13222	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqr00d 13223	A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( sqr ` A ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	absvalsqd 13224	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2d 13225	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	absge0d 13226	Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( abs ` A ) )
Theorem	absval2d 13227	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) = ( sqr ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
Theorem	abs00d 13228	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	absne0d 13229	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( abs ` A ) =/= 0 )
Theorem	absrpcld 13230	The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( abs ` A ) e. RR+ )
Theorem	absnegd 13231	Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscjd 13232	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 13233	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 13234	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 13235	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 13236	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 13237	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 13238	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 13239	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 13240	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 13241	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 13242	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 13243	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.9  Elementary limits and convergence
5.9.1  Superior limit (lim sup)
Syntax	clsp 13244	Extend class notation to include the limsup function.
class limsup
Definition	df-limsup 13245*	Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 13248 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 13246	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 13247	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 13248*	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 13249*	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 13250*	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 13251*	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 13252*	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 13253*	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 13254*	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 13255*	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 13256*	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 13257*	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.9.2  Limits
Syntax	cli 13258	Extend class notation with convergence relation for limits.
class ~~>
Syntax	crli 13259	Extend class notation with real convergence relation for limits.
class ~~> r
Syntax	co1 13260	Extend class notation with the set of all eventually bounded functions.
class O(1)
Syntax	clo1 13261	Extend class notation with the set of all eventually upper bounded functions.
class <_O(1)
Definition	df-clim 13262*	Define the limit relation for complex number sequences. See clim 13268 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 13263*	Define the limit relation for partial functions on the reals. See rlim 13269 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 13264*	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 13265*	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 13266	The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Rel ~~>
Theorem	rlimrel 13267	The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.)
|- Rel ~~> r
Theorem	clim 13268*	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 13269*	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 13270*	Rewrite rlim 13269 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 13271*	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 13272*	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 13273	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 13274	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 13275	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 13276	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 13277	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 13278*	Express the predicate: The limit of complex number sequence F is A, or F converges to A, with more general quantifier restrictions than clim 13268. (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 13279*	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 13280*	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 13281*	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 13282*	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 13283*	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 13284*	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 13285*	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 13286*	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 13287*	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 13288*	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 13289*	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 13290*	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 13291*	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 13292	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 13293	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 13294*	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 13295*	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 13296*	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 13297*	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 13298*	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 13299*	Refine o1bdd2 13315 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 13300*	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 ) )