P. 122 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12101-12200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	addcn2 12101*	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 and df-cncf are not yet available to us. See addcncntop 15788 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 12102*	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 12103*	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	reccn2ap 12104*	The reciprocal function is continuous. The class T is just for convenience in writing the proof and typically would be passed in as an instance of eqid 2238. (Contributed by Mario Carneiro, 9-Feb-2014.) Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.)
|- T = (inf ( { 1 , ( ( abs ` A ) x. B ) } , RR , < ) x. ( ( abs ` A ) / 2 ) )   =>    |- ( ( A e. CC /\ A # 0 /\ B e. RR+ ) -> E. y e. RR+ A. z e. { w e. CC | w # 0 } ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < B ) )
Theorem	cn1lem 12105*	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 12106*	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 12107*	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 12108*	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 12109*	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 12110*	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 12111*	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 12112*	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 12113*	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 12114*	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	climrecl 12115*	The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   =>    |- ( ph -> A e. RR )
Theorem	climge0 12116*	A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.)
|- 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	climadd 12117*	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 12118*	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 12119*	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 12120*	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 12121*	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 12122*	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 12123*	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 12124*	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 12125*	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 12126*	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 12127*	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	clim2ser 12128*	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 12129*	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 12130*	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 12131*	Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
|- 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 12132*	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 12133*	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 12134*	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 12135*	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 12136*	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	iser3shft 12137*	Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Jim Kingdon, 17-Oct-2022.)
|- ( ph -> F e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ~~> A <-> seq ( M + N ) ( .+ , ( F shift N ) ) ~~> A ) )
Theorem	climcau 12138*	A converging sequence of complex numbers is a Cauchy sequence. The converse would require excluded middle or a different definition of Cauchy sequence (for example, fixing a rate of convergence as in climcvg1n 12141). 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	climrecvg1n 12139*	A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within C / n of the nth term, where C is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( abs ` ( ( F ` k ) - ( F ` n ) ) ) < ( C / n ) )   =>    |- ( ph -> F e. dom ~~> )
Theorem	climcvg1nlem 12140*	Lemma for climcvg1n 12141. We construct sequences of the real and imaginary parts of each term of F, show those converge, and use that to show that F converges. (Contributed by Jim Kingdon, 24-Aug-2021.)
|- ( ph -> F : NN --> CC )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( abs ` ( ( F ` k ) - ( F ` n ) ) ) < ( C / n ) )   &    |- G = ( x e. NN |-> ( Re ` ( F ` x ) ) )   &    |- H = ( x e. NN |-> ( Im ` ( F ` x ) ) )   &    |- J = ( x e. NN |-> ( _i x. ( H ` x ) ) )   =>    |- ( ph -> F e. dom ~~> )
Theorem	climcvg1n 12141*	A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within C / n of the nth term, where C is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
|- ( ph -> F : NN --> CC )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( abs ` ( ( F ` k ) - ( F ` n ) ) ) < ( C / n ) )   =>    |- ( ph -> F e. dom ~~> )
Theorem	climcaucn 12142*	A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 12138 but adds the part that ( F ` k ) is complex. (Contributed by Jim Kingdon, 24-Aug-2021.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ 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 12143*	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 )
4.9.2  Finite and infinite sums
Syntax	csu 12144	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-sumdc 12145*	Define the sum of a series with an index set of integers A. The variable 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. In both cases we have an if expression so that we only need B to be defined where k e. A. In the infinite case, we also require that the indexing set be a decidable subset of an upperset of integers (that is, membership of integers in it is decidable). These two methods of summation produce the same result on their common region of definition (i.e., finite sets of integers). 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 12314). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)
|- sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m ) ) ) )
Theorem	sumeq1 12146	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 12147	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 12148	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	sumdc 12149*	Decidability of a subset of upper integers. (Contributed by Jim Kingdon, 1-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ph -> A. x e. ( ZZ>= ` M )DECID x e. A )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> DECID N e. A )
Theorem	sumeq2 12150*	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 12151	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 12152*	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 12153*	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 12154*	Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|- A = B   =>    |- sum_ k e. A C = sum_ k e. B C
Theorem	sumeq2i 12155*	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 12156*	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 12157*	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 12158*	Equality deduction for sum. Note that unlike sumeq2dv 12159, 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 12159*	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	sumeq2ad 12160*	Equality deduction for sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> B = C )   =>    |- ( ph -> sum_ k e. A B = sum_ k e. A C )
Theorem	sumeq2sdv 12161*	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 12162*	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 12163*	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 12164*	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	sumfct 12165*	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 Jim Kingdon, 18-Sep-2022.)
|- ( A. k e. A B e. CC -> sum_ j e. A ( ( k e. A |-> B ) ` j ) = sum_ k e. A B )
Theorem	fz1f1o 12166*	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	fzf1o 12167*	A finite set can be enumerated by integers starting at one. (Contributed by Jim Kingdon, 4-Apr-2026.)
|- ( A e. Fin -> E. f f : ( 1 ... (♯ ` A ) ) -1-1-onto-> A )
Theorem	nnf1o 12168	Lemma for sum and product theorems. (Contributed by Jim Kingdon, 15-Aug-2022.)
|- ( ph -> ( M e. NN /\ N e. NN ) )   &    |- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )   &    |- ( ph -> G : ( 1 ... N ) -1-1-onto-> A )   =>    |- ( ph -> N = M )
Theorem	sumrbdclem 12169*	Lemma for sumrbdc 12171. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 8-Apr-2023.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( + , F ) |` ( ZZ>= ` N ) ) = seq N ( + , F ) )
Theorem	fsum3cvg 12170*	The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 12-Nov-2022.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )
Theorem	sumrbdc 12171*	Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|- 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 /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> DECID k e. A )   =>    |- ( ph -> ( seq M ( + , F ) ~~> C <-> seq N ( + , F ) ~~> C ) )
Theorem	summodclem3 12172*	Lemma for summodc 12175. (Contributed by Mario Carneiro, 29-Mar-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> ( M e. NN /\ N e. NN ) )   &    |- ( ph -> f : ( 1 ... M ) -1-1-onto-> A )   &    |- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )   &    |- G = ( n e. NN |-> if ( n <_ M , [_ ( f ` n ) / k ]_ B , 0 ) )   &    |- H = ( n e. NN |-> if ( n <_ N , [_ ( K ` n ) / k ]_ B , 0 ) )   =>    |- ( ph -> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , H ) ` N ) )
Theorem	summodclem2a 12173*	Lemma for summodc 12175. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- G = ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 0 ) )   &    |- H = ( n e. NN |-> if ( n <_ N , [_ ( K ` n ) / k ]_ B , 0 ) )   &    |- ( 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	summodclem2 12174*	Lemma for summodc 12175. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 0 ) )   =>    |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ 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	summodc 12175*	A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 0 ) )   &    |- G = ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 0 ) )   =>    |- ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) )
Theorem	zsumdc 12176*	Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) (Revised by Jim Kingdon, 8-Apr-2023.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )   &    |- ( ph -> A. x e. Z DECID x e. A )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> sum_ k e. A B = ( ~~> ` seq M ( + , F ) ) )
Theorem	isum 12177*	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	fsumgcl 12178*	Closure for a function used to describe a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|- ( 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 -> A. n e. ( 1 ... M ) ( G ` n ) e. CC )
Theorem	fsum3 12179*	The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|- ( 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 ( + , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 0 ) ) ) ` M ) )
Theorem	sum0 12180	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	isumz 12181*	Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|- ( ( ( M e. ZZ /\ A C_ ( ZZ>= ` M ) /\ A. j e. ( ZZ>= ` M )DECID j e. A ) \/ A e. Fin ) -> sum_ k e. A 0 = 0 )
Theorem	fsumf1o 12182*	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	isumss 12183*	Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 21-Sep-2022.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )   &    |- ( ph -> A. j e. ( ZZ>= ` M )DECID j e. A )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> B C_ ( ZZ>= ` M ) )   &    |- ( ph -> A. j e. ( ZZ>= ` M )DECID j e. B )   =>    |- ( ph -> sum_ k e. A C = sum_ k e. B C )
Theorem	fisumss 12184*	Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )   &    |- ( ph -> A. j e. B DECID j e. A )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> sum_ k e. A C = sum_ k e. B C )
Theorem	isumss2 12185*	Change the index set of a sum by adding zeroes. The nonzero elements are in the contained set A and the added zeroes compose the rest of the containing set B which needs to be summable. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.)
|- ( ph -> A C_ B )   &    |- ( ph -> A. j e. B DECID j e. A )   &    |- ( ph -> A. k e. A C e. CC )   &    |- ( ph -> ( ( M e. ZZ /\ B C_ ( ZZ>= ` M ) /\ A. j e. ( ZZ>= ` M )DECID j e. B ) \/ B e. Fin ) )   =>    |- ( ph -> sum_ k e. A C = sum_ k e. B if ( k e. A , C , 0 ) )
Theorem	fsum3cvg2 12186*	The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|- ( ( 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 /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )
Theorem	fsumsersdc 12187*	Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Jim Kingdon, 5-May-2023.)
|- ( ( 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 /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> sum_ k e. A B = ( seq M ( + , F ) ` N ) )
Theorem	fsum3cvg3 12188*	A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ( 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	fsum3ser 12189*	A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 12204 and fsump1 12212, which should make our notation clear and from which, along with closure fsumcl 12192, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.)
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> A e. CC )   =>    |- ( ph -> sum_ k e. ( M ... N ) A = ( seq M ( + , F ) ` N ) )
Theorem	fsumcl2lem 12190*	- 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 12191*	- 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 12192*	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 12193*	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 12194*	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 )
Theorem	fsumnn0cl 12195*	Closure of a finite sum of nonnegative integers. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. NN0 )   =>    |- ( ph -> sum_ k e. A B e. NN0 )
Theorem	fsumrpcl 12196*	Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ k e. A ) -> B e. RR+ )   =>    |- ( ph -> sum_ k e. A B e. RR+ )
Theorem	fsumzcl2 12197*	A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018.)
|- ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> sum_ k e. A B e. ZZ )
Theorem	fsumadd 12198*	The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   =>    |- ( ph -> sum_ k e. A ( B + C ) = ( sum_ k e. A B + sum_ k e. A C ) )
Theorem	fsumsplit 12199*	Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.)
|- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> sum_ k e. U C = ( sum_ k e. A C + sum_ k e. B C ) )
Theorem	fsumsplitf 12200*	Split a sum into two parts. A version of fsumsplit 12199 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> sum_ k e. U C = ( sum_ k e. A C + sum_ k e. B C ) )