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	rlim2 13301*	Rewrite rlim 13300 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 13302*	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 13303*	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 13304	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 13305	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 13306	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 13307	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 13308	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 13309*	Express the predicate: The limit of complex number sequence F is A, or F converges to A, with more general quantifier restrictions than clim 13299. (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 13310*	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 13311*	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 13312*	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 13313*	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 13314*	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 13315*	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 13316*	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 13317*	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 13318*	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 13319*	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 13320*	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 13321*	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 13322*	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 13323	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 13324	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 13325*	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 13326*	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 13327*	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 13328*	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 13329*	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 13330*	Refine o1bdd2 13346 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 13331*	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 13332*	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 13333*	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 13334	An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( F e. O(1) -> F : dom F --> CC )
Theorem	o1dm 13335	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 13336*	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 13337	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 13338*	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 13339*	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 13340*	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 13341*	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 13342*	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 13343*	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 13344*	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 13345*	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 13346*	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 13347*	Refine o1bdd2 13346 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 13348*	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 13349*	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 13350	Forward direction of rlimclim 13351. (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 13351	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 13352*	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 13353	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 13354	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 13355	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 13356	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 13357	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 13358	The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ~~> : dom ~~> --> CC
Theorem	climdm 13359	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 13360*	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 13361*	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 13362*	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 13363	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 13364	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 13365	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 13366*	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 13367*	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 13368*	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 13369	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 13370	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 13371	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 13372*	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 13373*	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 13374*	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 13375*	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 13376*	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 13377*	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 13378*	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 13379	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 13380	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 13381	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 13382	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 13383*	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 13384*	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 13385*	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 13386*	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 13387*	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 13388*	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 13389*	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 13390*	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 13391*	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 13392*	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 13393*	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 ) )
Theorem	rlimcn1b 13394*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> ( k e. A |-> B ) ~~> 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 -> ( k e. A |-> ( F ` B ) ) ~~> r ( F ` C ) )
Theorem	rlimcn2 13395*	Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014.)
|- ( ( ph /\ z e. A ) -> B e. X )   &    |- ( ( ph /\ z e. A ) -> C e. Y )   &    |- ( ph -> R e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> ( z e. A |-> B ) ~~> r R )   &    |- ( ph -> ( z e. A |-> C ) ~~> r S )   &    |- ( ph -> F : ( X X. Y ) --> CC )   &    |- ( ( ph /\ x e. RR+ ) -> E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) )   =>    |- ( ph -> ( z e. A |-> ( B F C ) ) ~~> r ( R F S ) )
Theorem	climcn1 13396*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. B )   &    |- ( ( ph /\ z e. B ) -> ( F ` z ) e. CC )   &    |- ( ph -> G ~~> A )   &    |- ( ph -> H e. W )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. B )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( F ` ( G ` k ) ) )   =>    |- ( ph -> H ~~> ( F ` A ) )
Theorem	climcn2 13397*	Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. D )   &    |- ( ( ph /\ ( u e. C /\ v e. D ) ) -> ( u F v ) e. CC )   &    |- ( ph -> G ~~> A )   &    |- ( ph -> H ~~> B )   &    |- ( ph -> K e. W )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ E. z e. RR+ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. C )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) e. D )   &    |- ( ( ph /\ k e. Z ) -> ( K ` k ) = ( ( G ` k ) F ( H ` k ) ) )   =>    |- ( ph -> K ~~> ( A F B ) )
Theorem	addcn2 13398*	Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn 19706 and df-cncf 21360 are not yet available to us. See addcn 21347 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )
Theorem	subcn2 13399*	Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u - v ) - ( B - C ) ) ) < A ) )
Theorem	mulcn2 13400*	Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u x. v ) - ( B x. C ) ) ) < A ) )