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	cjcn2 13601*	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 13602*	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 13603*	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 13604*	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 13605*	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 13606*	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 13607*	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 13608*	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 13609*	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 13610*	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 13611*	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 13612*	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 13613*	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 13614*	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 13615	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 13616	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 13617	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 13618	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 13619	A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( F e. dom ~~> r -> F e. O(1) )
Theorem	o1rlimmul 13620	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 13621*	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 13622*	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 13623*	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 13624*	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 13625*	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 13626*	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 13627*	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 13628*	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 13629*	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 13630*	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 13631*	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 13632*	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 13628. (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 13633*	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 13634*	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 13635*	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 13636*	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 13637*	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 13638*	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 13639*	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 13640*	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 13641*	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 13642*	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 13643*	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 13644*	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 13645*	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 13646*	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 13647*	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 13648*	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 13649*	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 13650*	Lemma for rlimsqz 13651 and rlimsqz2 13652. (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 13651*	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 13652*	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 13653*	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 13654*	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 13655*	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 13656*	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 13657*	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 13658*	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 13659*	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 13660*	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 13661*	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 13662*	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 13663*	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 13664*	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 13665	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 13666*	Lemma for isercoll 13669. (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 13667*	Lemma for isercoll 13669. (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 13668*	Lemma for isercoll 13669. (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 13669*	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 13670*	Generalize isercoll 13669 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 13671*	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 , < ) )
Theorem	climcau 13672*	A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
Theorem	climbdd 13673*	A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x )
Theorem	caucvgrlem 13674*	Lemma for caurcvgr 13676. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   &    |- ( ph -> R e. RR+ )   =>    |- ( ph -> E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) ) )
Theorem	caucvgrlemOLD 13675*	Lemma for caurcvgr 13676. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.) Obsolete version of caucvgrlem 13674 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   &    |- ( ph -> R e. RR+ )   =>    |- ( ph -> E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) ) )
Theorem	caurcvgr 13676*	A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that F is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016.) (Revised by AV, 12-Sep-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   =>    |- ( ph -> F ~~> r ( limsup ` F ) )
Theorem	caurcvgrOLD 13677*	A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that F is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016.) Obsolete version of caurcvgr 13676 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   =>    |- ( ph -> F ~~> r ( limsup ` F ) )
Theorem	caucvgrlem2 13678*	Lemma for caucvgr 13679. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Mario Carneiro, 8-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   &    |- H : CC --> RR   &    |- ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )   =>    |- ( ph -> ( n e. A |-> ( H ` ( F ` n ) ) ) ~~> r ( ~~> r ` ( H o. F ) ) )
Theorem	caucvgr 13679*	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 8-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   =>    |- ( ph -> F e. dom ~~> r )
Theorem	caurcvg 13680*	A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that F is a Cauchy sequence. (Contributed by NM, 4-Apr-2005.) (Revised by AV, 12-Sep-2020.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ph -> A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )   =>    |- ( ph -> F ~~> ( limsup ` F ) )
Theorem	caurcvgOLD 13681*	A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that F is a Cauchy sequence. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 8-May-2016.) Obsolete version of caurcvg 13680 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ph -> A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )   =>    |- ( ph -> F ~~> ( limsup ` F ) )
Theorem	caurcvg2 13682*	A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 7-Sep-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   =>    |- ( ph -> F e. dom ~~> )
Theorem	caucvg 13683*	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Proof shortened by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )   &    |- ( ph -> F e. V )   =>    |- ( ph -> F e. dom ~~> )
Theorem	caucvgb 13684*	A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of [Gleason] p. 180. (Contributed by Mario Carneiro, 15-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ F e. V ) -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
Theorem	serf0 13685*	If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> F ~~> 0 )
Theorem	iseraltlem1 13686*	Lemma for iseralt 13689. A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )   &    |- ( ph -> G ~~> 0 )   =>    |- ( ( ph /\ N e. Z ) -> 0 <_ ( G ` N ) )
Theorem	iseraltlem2 13687*	Lemma for iseralt 13689. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example S ( 1 ) <_ S ( 3 ) <_ S ( 5 ) <_ ... and ... <_ S ( 4 ) <_ S ( 2 ) <_ S ( 0 ) (assuming M = 0 so that these terms are defined). (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )   &    |- ( ph -> G ~~> 0 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )   =>    |- ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) )
Theorem	iseraltlem3 13688*	Lemma for iseralt 13689. From iseraltlem2 13687, we have ( -u 1 ^ n ) x. S ( n + 2 k ) <_ ( -u 1 ^ n ) x. S ( n ) and ( -u 1 ^ n ) x. S ( n + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k + 1 ), and we also have ( -u 1 ^ n ) x. S ( n + 1 ) = ( -u 1 ^ n ) x. S ( n ) - G ( n + 1 ) for each n by the definition of the partial sum S, so combining the inequalities we get ( -u 1 ^ n ) x. S ( n ) - G ( n + 1 ) = ( -u 1 ^ n ) x. S ( n + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) = ( -u 1 ^ n ) x. S ( n + 2 k ) - G ( n + 2 k + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k ) <_ ( -u 1 ^ n ) x. S ( n ) <_ ( -u 1 ^ n ) x. S ( n ) + G ( n + 1 ), so | ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) - ( -u 1 ^ n ) x. S ( n ) | = | S ( n + 2 k + 1 ) - S ( n ) | <_ G ( n + 1 ) and | ( -u 1 ^ n ) x. S ( n + 2 k ) - ( -u 1 ^ n ) x. S ( n ) | = | S ( n + 2 k ) - S ( n ) | <_ G ( n + 1 ). Thus, both even and odd partial sums are Cauchy if G converges to 0. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )   &    |- ( ph -> G ~~> 0 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )   =>    |- ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) <_ ( G ` ( N + 1 ) ) /\ ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) <_ ( G ` ( N + 1 ) ) ) )
Theorem	iseralt 13689*	The alternating series test. If G ( k ) is a decreasing sequence that converges to 0, then sum_ k e. Z ( -u 1 ^ k ) x. G ( k ) is a convergent series. (Note that the first term is positive if M is even, and negative if M is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -u 1 using isermulc2 13659.) (Contributed by Mario Carneiro, 7-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )   &    |- ( ph -> G ~~> 0 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )   =>    |- ( ph -> seq M ( + , F ) e. dom ~~> )
5.10.3  Finite and infinite sums
Syntax	csu 13690	Extend class notation to include finite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.)
class sum_ k e. A B
Definition	df-sum 13691*	Define the sum of a series with an index set of integers A. k is normally a free variable in B, i.e. B can be thought of as B ( k ). This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers) by summo 13721. Examples: sum_ k e. { 1 , 2 , 4 } k means 1 + 2 + 4 = 7, and sum_ k e. NN ( 1 / ( 2 ^ k ) ) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 13876). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|- sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
Theorem	sumex 13692	A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|- sum_ k e. A B e. _V
Theorem	sumeq1 13693	Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|- ( A = B -> sum_ k e. A C = sum_ k e. B C )
Theorem	nfsum1 13694	Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|- F/_ k A   =>    |- F/_ k sum_ k e. A B
Theorem	nfsum 13695	Bound-variable hypothesis builder for sum: if x is (effectively) not free in A and B, it is not free in sum_ k e. A B. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x sum_ k e. A B
Theorem	sumeq2w 13696	Equality theorem for sum, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro, 13-Jun-2019.)
|- ( A. k B = C -> sum_ k e. A B = sum_ k e. A C )
Theorem	sumeq2ii 13697*	Equality theorem for sum, with the class expressions B and C guarded by _I to be always sets. (Contributed by Mario Carneiro, 13-Jun-2019.)
|- ( A. k e. A ( _I ` B ) = ( _I ` C ) -> sum_ k e. A B = sum_ k e. A C )
Theorem	sumeq2 13698*	Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( A. k e. A B = C -> sum_ k e. A B = sum_ k e. A C )
Theorem	cbvsum 13699*	Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|- ( j = k -> B = C )   &    |- F/_ k A   &    |- F/_ j A   &    |- F/_ k B   &    |- F/_ j C   =>    |- sum_ j e. A B = sum_ k e. A C
Theorem	cbvsumv 13700*	Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( j = k -> B = C )   =>    |- sum_ j e. A B = sum_ k e. A C