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	lo1dm 13301	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 13302*	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 13303*	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 13304*	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 13305*	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 13306*	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 13307*	Refine o1bdd2 13323 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 13308*	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 13309*	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 13310*	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 13311	An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( F e. O(1) -> F : dom F --> CC )
Theorem	o1dm 13312	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 13313*	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 13314	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 13315*	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 13316*	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 13317*	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 13318*	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 13319*	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 13320*	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 13321*	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 13322*	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 13323*	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 13324*	Refine o1bdd2 13323 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 13325*	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 13326*	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 13327	Forward direction of rlimclim 13328. (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 13328	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 13329*	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 13330	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 13331	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 13332	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 13333	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 13334	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 13335	The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ~~> : dom ~~> --> CC
Theorem	climdm 13336	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 13337*	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 13338*	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 13339*	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 13340	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 13341	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 13342	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 13343*	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 13344*	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 13345*	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 13346	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 13347	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 13348	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 13349*	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 13350*	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 13351*	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 13352*	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 13353*	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 13354*	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 13355*	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 13356	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 13357	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 13358	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 13359	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 13360*	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 13361*	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 13362*	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 13363*	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 13364*	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 13365*	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 13366*	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 13367*	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 13368*	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 13369*	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 13370*	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 13371*	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 13372*	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 13373*	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 13374*	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 13375*	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 19494 and df-cncf 21117 are not yet available to us. See addcn 21104 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 13376*	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 13377*	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 ) )
Theorem	reccn2 13378*	The reciprocal function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) (Revised by Mario Carneiro, 22-Sep-2014.)
|- T = ( if ( 1 <_ ( ( abs ` A ) x. B ) , 1 , ( ( abs ` A ) x. B ) ) x. ( ( abs ` A ) / 2 ) )   =>    |- ( ( A e. ( CC \ { 0 } ) /\ B e. RR+ ) -> E. y e. RR+ A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < B ) )
Theorem	cn1lem 13379*	A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- F : CC --> CC   &    |- ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) <_ ( abs ` ( z - A ) ) )   =>    |- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
Theorem	abscn2 13380*	The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( abs ` z ) - ( abs ` A ) ) ) < x ) )
Theorem	cjcn2 13381*	The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( * ` z ) - ( * ` A ) ) ) < x ) )
Theorem	recn2 13382*	The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Re ` z ) - ( Re ` A ) ) ) < x ) )
Theorem	imcn2 13383*	The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Im ` z ) - ( Im ` A ) ) ) < x ) )
Theorem	climcn1lem 13384*	The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- H : CC --> CC   &    |- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( H ` z ) - ( H ` A ) ) ) < x ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( H ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( H ` A ) )
Theorem	climabs 13385*	Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( abs ` A ) )
Theorem	climcj 13386*	Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( * ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( * ` A ) )
Theorem	climre 13387*	Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( Re ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( Re ` A ) )
Theorem	climim 13388*	Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( Im ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( Im ` A ) )
Theorem	rlimmptrcl 13389*	Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ( ph /\ k e. A ) -> B e. CC )
Theorem	rlimabs 13390*	Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> ( abs ` B ) ) ~~> r ( abs ` C ) )
Theorem	rlimcj 13391*	Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> ( * ` B ) ) ~~> r ( * ` C ) )
Theorem	rlimre 13392*	Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> ( Re ` B ) ) ~~> r ( Re ` C ) )
Theorem	rlimim 13393*	Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> ( Im ` B ) ) ~~> r ( Im ` C ) )
Theorem	o1of2 13394*	Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( m e. RR /\ n e. RR ) -> M e. RR )   &    |- ( ( x e. CC /\ y e. CC ) -> ( x R y ) e. CC )   &    |- ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) ) -> ( ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) -> ( abs ` ( x R y ) ) <_ M ) )   =>    |- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF R G ) e. O(1) )
Theorem	o1add 13395	The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
|- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF + G ) e. O(1) )
Theorem	o1mul 13396	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
|- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF x. G ) e. O(1) )
Theorem	o1sub 13397	The difference of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
|- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF - G ) e. O(1) )
Theorem	rlimo1 13398	Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( F ~~> r A -> F e. O(1) )
Theorem	rlimdmo1 13399	A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( F e. dom ~~> r -> F e. O(1) )
Theorem	o1rlimmul 13400	The product of an eventually bounded function and a function of limit zero has limit zero. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( ( F e. O(1) /\ G ~~> r 0 ) -> ( F oF x. G ) ~~> r 0 )