P. 144 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14301-14400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	o1eq 14301*	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 14302*	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 14303*	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 14304*	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 14305	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 14306	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 14307	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 14308	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 14309*	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 14310*	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 14311*	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 14312*	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 14313*	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 14314*	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 14315*	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 14316*	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 14317*	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 14318*	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 14319*	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 14320*	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 14321*	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 14322*	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 14323*	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 14324*	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 21031 and df-cncf 22681 are not yet available to us. See addcn 22668 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 14325*	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 14326*	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 14327*	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 14328*	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 14329*	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 14330*	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 14331*	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 14332*	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 14333*	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 14334*	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 14335*	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 14336*	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 14337*	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 14338*	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 14339*	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 14340*	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 14341*	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 14342*	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 14343*	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 14344	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 14345	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 14346	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 14347	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 14348	A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( F e. dom ~~> r -> F e. O(1) )
Theorem	o1rlimmul 14349	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 14350*	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 14351*	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 14352*	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 14353*	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 14354*	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 14355*	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 14356*	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 14357*	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 14358*	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 14359*	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 14360*	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 14361*	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 14357. (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 14362*	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 14363*	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 14364*	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 14365*	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 14366*	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 14367*	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 14368*	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 14369*	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 14370*	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 14371*	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 14372*	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 14373*	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 14374*	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 14375*	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 14376*	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 14377*	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 14378*	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 14379*	Lemma for rlimsqz 14380 and rlimsqz2 14381. (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 14380*	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 14381*	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 14382*	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 14383*	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 14384*	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 14385*	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 14386*	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 14387*	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 14388*	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 14389*	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 )
Theorem	iserle 14390*	Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ph -> seq M ( + , 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	iserge0 14391*	The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )   =>    |- ( ph -> 0 <_ A )
Theorem	climub 14392*	The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )   =>    |- ( ph -> ( F ` N ) <_ A )
Theorem	climserle 14393*	The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by NM, 27-Dec-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )   =>    |- ( ph -> ( seq M ( + , F ) ` N ) <_ A )
Theorem	isershft 14394	Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( M e. ZZ /\ N e. ZZ ) -> ( seq M ( .+ , F ) ~~> A <-> seq ( M + N ) ( .+ , ( F shift N ) ) ~~> A ) )
Theorem	isercolllem1 14395*	Lemma for isercoll 14398. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : NN --> Z )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   =>    |- ( ( ph /\ S C_ NN ) -> ( G |` S ) Isom < , < ( S , ( G " S ) ) )
Theorem	isercolllem2 14396*	Lemma for isercoll 14398. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : NN --> Z )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   =>    |- ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) = ( `' G " ( M ... N ) ) )
Theorem	isercolllem3 14397*	Lemma for isercoll 14398. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : NN --> Z )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   &    |- ( ( ph /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )   &    |- ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( H ` k ) = ( F ` ( G ` k ) ) )   =>    |- ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( seq M ( + , F ) ` N ) = ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) )
Theorem	isercoll 14398*	Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : NN --> Z )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   &    |- ( ( ph /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )   &    |- ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( H ` k ) = ( F ` ( G ` k ) ) )   =>    |- ( ph -> ( seq 1 ( + , H ) ~~> A <-> seq M ( + , F ) ~~> A ) )
Theorem	isercoll2 14399*	Generalize isercoll 14398 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> G : Z --> W )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   &    |- ( ( ph /\ n e. ( W \ ran G ) ) -> ( F ` n ) = 0 )   &    |- ( ( ph /\ n e. W ) -> ( F ` n ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( F ` ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( + , H ) ~~> A <-> seq N ( + , F ) ~~> A ) )
Theorem	climsup 14400*	A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )   &    |- ( ph -> E. x e. RR A. k e. Z ( F ` k ) <_ x )   =>    |- ( ph -> F ~~> sup ( ran F , RR , < ) )