P. 138 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13701-13800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	climsubc2 13701*	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 13702*	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 13703*	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 13704*	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 13705*	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 13706*	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 13707*	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 13708*	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 13709*	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 13710*	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 13711*	Lemma for rlimsqz 13712 and rlimsqz2 13713. (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 13712*	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 13713*	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 13714*	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 13715*	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 13716*	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 13717*	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 13718*	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 13719*	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 13720*	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 13721*	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 13722*	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 13723*	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 13724*	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 13725*	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 13726	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 13727*	Lemma for isercoll 13730. (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 13728*	Lemma for isercoll 13730. (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 13729*	Lemma for isercoll 13730. (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 13730*	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 13731*	Generalize isercoll 13730 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 13732*	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 13733*	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 13734*	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 13735*	Lemma for caurcvgr 13737. (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 13736*	Lemma for caurcvgr 13737. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.) Obsolete version of caucvgrlem 13735 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 13737*	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 13738*	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 13737 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 13739*	Lemma for caucvgr 13740. (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 13740*	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 13741*	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 13742*	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 13741 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 13743*	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 13744*	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 13745*	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 13746*	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 13747*	Lemma for iseralt 13750. 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 13748*	Lemma for iseralt 13750. 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 13749*	Lemma for iseralt 13750. From iseraltlem2 13748, 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 13750*	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 13720.) (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 13751	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 13752*	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 13782. 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 13937). (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 13753	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 13754	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 13755	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 13756	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 13757	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 13758*	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 13759*	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 13760*	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 13761*	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
Theorem	cbvsumi 13762*	Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
|- F/_ k B   &    |- F/_ j C   &    |- ( j = k -> B = C )   =>    |- sum_ j e. A B = sum_ k e. A C
Theorem	sumeq1i 13763*	Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|- A = B   =>    |- sum_ k e. A C = sum_ k e. B C
Theorem	sumeq2i 13764*	Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
|- ( k e. A -> B = C )   =>    |- sum_ k e. A B = sum_ k e. A C
Theorem	sumeq12i 13765*	Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|- A = B   &    |- ( k e. A -> C = D )   =>    |- sum_ k e. A C = sum_ k e. B D
Theorem	sumeq1d 13766*	Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
|- ( ph -> A = B )   =>    |- ( ph -> sum_ k e. A C = sum_ k e. B C )
Theorem	sumeq2d 13767*	Equality deduction for sum. Note that unlike sumeq2dv 13768, k may occur in ph. (Contributed by NM, 1-Nov-2005.)
|- ( ph -> A. k e. A B = C )   =>    |- ( ph -> sum_ k e. A B = sum_ k e. A C )
Theorem	sumeq2dv 13768*	Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- ( ( ph /\ k e. A ) -> B = C )   =>    |- ( ph -> sum_ k e. A B = sum_ k e. A C )
Theorem	sumeq2sdv 13769*	Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
|- ( ph -> B = C )   =>    |- ( ph -> sum_ k e. A B = sum_ k e. A C )
Theorem	2sumeq2dv 13770*	Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- ( ( ph /\ j e. A /\ k e. B ) -> C = D )   =>    |- ( ph -> sum_ j e. A sum_ k e. B C = sum_ j e. A sum_ k e. B D )
Theorem	sumeq12dv 13771*	Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|- ( ph -> A = B )   &    |- ( ( ph /\ k e. A ) -> C = D )   =>    |- ( ph -> sum_ k e. A C = sum_ k e. B D )
Theorem	sumeq12rdv 13772*	Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|- ( ph -> A = B )   &    |- ( ( ph /\ k e. B ) -> C = D )   =>    |- ( ph -> sum_ k e. A C = sum_ k e. B D )
Theorem	sum2id 13773*	The second class argument to a sum can be chosen so that it is always a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- sum_ k e. A B = sum_ k e. A ( _I ` B )
Theorem	sumfc 13774*	A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- sum_ j e. A ( ( k e. A |-> B ) ` j ) = sum_ k e. A B
Theorem	fz1f1o 13775*	A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.)
|- ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
Theorem	sumrblem 13776*	Lemma for sumrb 13778. (Contributed by Mario Carneiro, 12-Aug-2013.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( + , F ) |` ( ZZ>= ` N ) ) = seq N ( + , F ) )
Theorem	fsumcvg 13777*	The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )
Theorem	sumrb 13778*	Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 9-Apr-2014.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ph -> A C_ ( ZZ>= ` N ) )   =>    |- ( ph -> ( seq M ( + , F ) ~~> C <-> seq N ( + , F ) ~~> C ) )
Theorem	summolem3 13779*	Lemma for summo 13782. (Contributed by Mario Carneiro, 29-Mar-2014.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )   &    |- H = ( n e. NN |-> [_ ( K ` n ) / k ]_ B )   &    |- ( ph -> ( M e. NN /\ N e. NN ) )   &    |- ( ph -> f : ( 1 ... M ) -1-1-onto-> A )   &    |- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )   =>    |- ( ph -> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , H ) ` N ) )
Theorem	summolem2a 13780*	Lemma for summo 13782. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 20-Apr-2014.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )   &    |- H = ( n e. NN |-> [_ ( K ` n ) / k ]_ B )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ph -> f : ( 1 ... N ) -1-1-onto-> A )   &    |- ( ph -> K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )   =>    |- ( ph -> seq M ( + , F ) ~~> ( seq 1 ( + , G ) ` N ) )
Theorem	summolem2 13781*	Lemma for summo 13782. (Contributed by Mario Carneiro, 3-Apr-2014.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )   =>    |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
Theorem	summo 13782*	A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )   =>    |- ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) )
Theorem	zsum 13783*	Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> sum_ k e. A B = ( ~~> ` seq M ( + , F ) ) )
Theorem	isum 13784*	Series sum with an upper integer index set (i.e. an infinite series). (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 7-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> sum_ k e. Z B = ( ~~> ` seq M ( + , F ) ) )
Theorem	fsum 13785*	The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Mario Carneiro, 13-Jun-2019.)
|- ( k = ( F ` n ) -> B = C )   &    |- ( ph -> M e. NN )   &    |- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )   =>    |- ( ph -> sum_ k e. A B = ( seq 1 ( + , G ) ` M ) )
Theorem	sum0 13786	Any sum over the empty set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|- sum_ k e. (/) A = 0
Theorem	sumz 13787*	Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|- ( ( A C_ ( ZZ>= ` M ) \/ A e. Fin ) -> sum_ k e. A 0 = 0 )
Theorem	fsumf1o 13788*	Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.)
|- ( k = G -> B = D )   &    |- ( ph -> C e. Fin )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ( ph /\ n e. C ) -> ( F ` n ) = G )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> sum_ k e. A B = sum_ n e. C D )
Theorem	sumss 13789*	Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )   &    |- ( ph -> B C_ ( ZZ>= ` M ) )   =>    |- ( ph -> sum_ k e. A C = sum_ k e. B C )
Theorem	fsumss 13790*	Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> sum_ k e. A C = sum_ k e. B C )
Theorem	sumss2 13791*	Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|- ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ ( B C_ ( ZZ>= ` M ) \/ B e. Fin ) ) -> sum_ k e. A C = sum_ k e. B if ( k e. A , C , 0 ) )
Theorem	fsumcvg2 13792*	The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.)
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )
Theorem	fsumsers 13793*	Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 21-Apr-2014.)
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> sum_ k e. A B = ( seq M ( + , F ) ` N ) )
Theorem	fsumcvg3 13794*	A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> seq M ( + , F ) e. dom ~~> )
Theorem	fsumser 13795*	A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition of follows as fsum1 13807 and fsump1i 13829, which should make our notation clear and from which, along with closure fsumcl 13798, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   =>    |- ( ph -> sum_ k e. ( M ... N ) A = ( seq M ( + , F ) ` N ) )
Theorem	fsumcl2lem 13796*	- Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by Mario Carneiro, 3-Jun-2014.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> sum_ k e. A B e. S )
Theorem	fsumcllem 13797*	- Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 3-Jun-2014.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> 0 e. S )   =>    |- ( ph -> sum_ k e. A B e. S )
Theorem	fsumcl 13798*	Closure of a finite sum of complex numbers A ( k ). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> sum_ k e. A B e. CC )
Theorem	fsumrecl 13799*	Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   =>    |- ( ph -> sum_ k e. A B e. RR )
Theorem	fsumzcl 13800*	Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ZZ )   =>    |- ( ph -> sum_ k e. A B e. ZZ )