P. 137 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	lo1res 13601	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 13602	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 13603*	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 13604*	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 13605*	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 13606	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 13607	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 13608	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 13609*	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 13610*	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 13611*	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 13612*	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 13613*	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 13614*	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 13615*	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 13616	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 13617	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 13618	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 13619	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 13620*	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 13621*	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 13622*	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 13623*	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 13624*	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 13625*	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 13626*	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 13627*	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 13628*	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 13629*	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 13630*	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 13631*	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 13632*	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 13633*	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 13634*	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 13635*	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 20174 and df-cncf 21806 are not yet available to us. See addcn 21793 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 13636*	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 13637*	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 13638*	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 13639*	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 13640*	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 13641*	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 13642*	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 13643*	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 13644*	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 13645*	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 13646*	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 13647*	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 13648*	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 13649*	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 13650*	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 13651*	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 13652*	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 13653*	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 13654*	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 13655	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 13656	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 13657	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 13658	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 13659	A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( F e. dom ~~> r -> F e. O(1) )
Theorem	o1rlimmul 13660	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 )
Theorem	o1const 13661*	A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( ( A C_ RR /\ B e. CC ) -> ( x e. A |-> B ) e. O(1) )
Theorem	lo1const 13662*	A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( A C_ RR /\ B e. RR ) -> ( x e. A |-> B ) e. <_O(1) )
Theorem	lo1mptrcl 13663*	Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   =>    |- ( ( ph /\ x e. A ) -> B e. RR )
Theorem	o1mptrcl 13664*	Reverse closure for an eventually bounded function. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   =>    |- ( ( ph /\ x e. A ) -> B e. CC )
Theorem	o1add2 13665*	The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B + C ) ) e. O(1) )
Theorem	o1mul2 13666*	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B x. C ) ) e. O(1) )
Theorem	o1sub2 13667*	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B - C ) ) e. O(1) )
Theorem	lo1add 13668*	The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )   =>    |- ( ph -> ( x e. A |-> ( B + C ) ) e. <_O(1) )
Theorem	lo1mul 13669*	The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> ( x e. A |-> ( B x. C ) ) e. <_O(1) )
Theorem	lo1mul2 13670*	The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> ( x e. A |-> ( C x. B ) ) e. <_O(1) )
Theorem	o1dif 13671*	If the difference of two functions is eventually bounded, eventual boundedness of either one implies the other. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ph -> ( x e. A |-> ( B - C ) ) e. O(1) )   =>    |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> C ) e. O(1) ) )
Theorem	lo1sub 13672*	The difference of an eventually upper bounded function and an eventually bounded function is eventually upper bounded. The "correct" sharp result here takes the second function to be eventually lower bounded instead of just bounded, but our notation for this is simply ( x e. A |-> -u C ) e. <_O(1), so it is just a special case of lo1add 13668. (Contributed by Mario Carneiro, 31-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B - C ) ) e. <_O(1) )
Theorem	climadd 13673*	Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> H e. X )   &    |- ( ph -> G ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) )   =>    |- ( ph -> H ~~> ( A + B ) )
Theorem	climmul 13674*	Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> H e. X )   &    |- ( ph -> G ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> H ~~> ( A x. B ) )
Theorem	climsub 13675*	Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> H e. X )   &    |- ( ph -> G ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) - ( G ` k ) ) )   =>    |- ( ph -> H ~~> ( A - B ) )
Theorem	climaddc1 13676*	Limit of a constant C added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( ( F ` k ) + C ) )   =>    |- ( ph -> G ~~> ( A + C ) )
Theorem	climaddc2 13677*	Limit of a constant C added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C + ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( C + A ) )
Theorem	climmulc2 13678*	Limit of a sequence multiplied by a constant C. Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C x. ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( C x. A ) )
Theorem	climsubc1 13679*	Limit of a constant C subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( ( F ` k ) - C ) )   =>    |- ( ph -> G ~~> ( A - C ) )
Theorem	climsubc2 13680*	Limit of a constant C minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C - ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( C - A ) )
Theorem	climle 13681*	Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )   =>    |- ( ph -> A <_ B )
Theorem	climsqz 13682*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) <_ A )   =>    |- ( ph -> G ~~> A )
Theorem	climsqz2 13683*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) <_ ( F ` k ) )   &    |- ( ( ph /\ k e. Z ) -> A <_ ( G ` k ) )   =>    |- ( ph -> G ~~> A )
Theorem	rlimadd 13684*	Limit of the sum of two converging functions. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   =>    |- ( ph -> ( x e. A |-> ( B + C ) ) ~~> r ( D + E ) )
Theorem	rlimsub 13685*	Limit of the difference of two converging functions. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   =>    |- ( ph -> ( x e. A |-> ( B - C ) ) ~~> r ( D - E ) )
Theorem	rlimmul 13686*	Limit of the product of two converging functions. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   =>    |- ( ph -> ( x e. A |-> ( B x. C ) ) ~~> r ( D x. E ) )
Theorem	rlimdiv 13687*	Limit of the quotient of two converging functions. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   &    |- ( ph -> E =/= 0 )   &    |- ( ( ph /\ x e. A ) -> C =/= 0 )   =>    |- ( ph -> ( x e. A |-> ( B / C ) ) ~~> r ( D / E ) )
Theorem	rlimneg 13688*	Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> -u B ) ~~> r -u C )
Theorem	rlimle 13689*	Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B <_ C )   =>    |- ( ph -> D <_ E )
Theorem	rlimsqzlem 13690*	Lemma for rlimsqz 13691 and rlimsqz2 13692. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.)
|- ( ph -> M e. RR )   &    |- ( ph -> E e. CC )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) )   =>    |- ( ph -> ( x e. A |-> C ) ~~> r E )
Theorem	rlimsqz 13691*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.)
|- ( ph -> D e. RR )   &    |- ( ph -> M e. RR )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> B <_ C )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ D )   =>    |- ( ph -> ( x e. A |-> C ) ~~> r D )
Theorem	rlimsqz2 13692*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 3-Feb-2014.) (Revised by Mario Carneiro, 20-May-2016.)
|- ( ph -> D e. RR )   &    |- ( ph -> M e. RR )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ B )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> D <_ C )   =>    |- ( ph -> ( x e. A |-> C ) ~~> r D )
Theorem	lo1le 13693*	Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ph -> M e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ B )   =>    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )
Theorem	o1le 13694*	Transfer eventual boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 25-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( ph -> M e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` C ) <_ ( abs ` B ) )   =>    |- ( ph -> ( x e. A |-> C ) e. O(1) )
Theorem	rlimno1 13695*	A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> ( x e. A |-> ( 1 / B ) ) ~~> r 0 )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> B =/= 0 )   =>    |- ( ph -> -. ( x e. A |-> B ) e. O(1) )
Theorem	clim2ser 13696*	The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> seq M ( + , F ) ~~> A )   =>    |- ( ph -> seq ( N + 1 ) ( + , F ) ~~> ( A - ( seq M ( + , F ) ` N ) ) )
Theorem	clim2ser2 13697*	The limit of an infinite series with an initial segment added. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> seq ( N + 1 ) ( + , F ) ~~> A )   =>    |- ( ph -> seq M ( + , F ) ~~> ( A + ( seq M ( + , F ) ` N ) ) )
Theorem	iserex 13698*	An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
Theorem	isermulc2 13699*	Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. CC )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C x. ( F ` k ) ) )   =>    |- ( ph -> seq M ( + , G ) ~~> ( C x. A ) )
Theorem	climlec2 13700*	Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> F ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> A <_ ( F ` k ) )   =>    |- ( ph -> A <_ B )