P. 121 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12001-12100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sumrbdclem 12001*	Lemma for sumrbdc 12003. (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 12002*	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 12003*	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 12004*	Lemma for summodc 12007. (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 12005*	Lemma for summodc 12007. (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 12006*	Lemma for summodc 12007. (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 12007*	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 12008*	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 12009*	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 12010*	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 12011*	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 12012	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 12013*	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 12014*	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 12015*	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 12016*	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 12017*	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 12018*	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 12019*	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 12020*	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 12021*	A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 12036 and fsump1 12044, which should make our notation clear and from which, along with closure fsumcl 12024, 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 12022*	- 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 12023*	- 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 12024*	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 12025*	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 12026*	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 12027*	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 12028*	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 12029*	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 12030*	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 12031*	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 12032*	Split a sum into two parts. A version of fsumsplit 12031 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 ) )
Theorem	sumsnf 12033*	A sum of a singleton is the term. A version of sumsn 12035 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/_ k B   &    |- ( k = M -> A = B )   =>    |- ( ( M e. V /\ B e. CC ) -> sum_ k e. { M } A = B )
Theorem	fsumsplitsn 12034*	Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( k = B -> C = D )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> sum_ k e. ( A u. { B } ) C = ( sum_ k e. A C + D ) )
Theorem	sumsn 12035*	A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.)
|- ( k = M -> A = B )   =>    |- ( ( M e. V /\ B e. CC ) -> sum_ k e. { M } A = B )
Theorem	fsum1 12036*	The finite sum of A ( k ) from k = M to M (i.e. a sum with only one term) is B i.e. A ( M ). (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
|- ( k = M -> A = B )   =>    |- ( ( M e. ZZ /\ B e. CC ) -> sum_ k e. ( M ... M ) A = B )
Theorem	sumpr 12037*	A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016.)
|- ( k = A -> C = D )   &    |- ( k = B -> C = E )   &    |- ( ph -> ( D e. CC /\ E e. CC ) )   &    |- ( ph -> ( A e. V /\ B e. W ) )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> sum_ k e. { A , B } C = ( D + E ) )
Theorem	sumtp 12038*	A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.)
|- ( k = A -> D = E )   &    |- ( k = B -> D = F )   &    |- ( k = C -> D = G )   &    |- ( ph -> ( E e. CC /\ F e. CC /\ G e. CC ) )   &    |- ( ph -> ( A e. V /\ B e. W /\ C e. X ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> A =/= C )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> sum_ k e. { A , B , C } D = ( ( E + F ) + G ) )
Theorem	sumsns 12039*	A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.)
|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> sum_ k e. { M } A = [_ M / k ]_ A )
Theorem	fsumm1 12040*	Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( k = N -> A = B )   =>    |- ( ph -> sum_ k e. ( M ... N ) A = ( sum_ k e. ( M ... ( N - 1 ) ) A + B ) )
Theorem	fzosump1 12041*	Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( k = N -> A = B )   =>    |- ( ph -> sum_ k e. ( M..^ ( N + 1 ) ) A = ( sum_ k e. ( M..^ N ) A + B ) )
Theorem	fsum1p 12042*	Separate out the first term in a finite sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( k = M -> A = B )   =>    |- ( ph -> sum_ k e. ( M ... N ) A = ( B + sum_ k e. ( ( M + 1 ) ... N ) A ) )
Theorem	fsumsplitsnun 12043*	Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by AV, 17-Dec-2021.)
|- ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> sum_ k e. ( A u. { Z } ) B = ( sum_ k e. A B + [_ Z / k ]_ B ) )
Theorem	fsump1 12044*	The addition of the next term in a finite sum of A ( k ) is the current term plus B i.e. A ( N + 1 ). (Contributed by NM, 4-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   &    |- ( k = ( N + 1 ) -> A = B )   =>    |- ( ph -> sum_ k e. ( M ... ( N + 1 ) ) A = ( sum_ k e. ( M ... N ) A + B ) )
Theorem	isumclim 12045*	An infinite sum equals the value its series converges to. (Contributed by NM, 25-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) ~~> B )   =>    |- ( ph -> sum_ k e. Z A = B )
Theorem	isumclim2 12046*	A converging series converges to its infinite sum. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )
Theorem	isumclim3 12047*	The sequence of partial finite sums of a converging infinite series converges to the infinite sum of the series. Note that j must not occur in A. (Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. dom ~~> )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ( ph /\ j e. Z ) -> ( F ` j ) = sum_ k e. ( M ... j ) A )   =>    |- ( ph -> F ~~> sum_ k e. Z A )
Theorem	sumnul 12048*	The sum of a non-convergent infinite series evaluates to the empty set. (Contributed by Paul Chapman, 4-Nov-2007.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> -. seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z A = (/) )
Theorem	isumcl 12049*	The sum of a converging infinite series is a complex number. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z A e. CC )
Theorem	isummulc2 12050*	An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( B x. sum_ k e. Z A ) = sum_ k e. Z ( B x. A ) )
Theorem	isummulc1 12051*	An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( sum_ k e. Z A x. B ) = sum_ k e. Z ( A x. B ) )
Theorem	isumdivapc 12052*	An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( sum_ k e. Z A / B ) = sum_ k e. Z ( A / B ) )
Theorem	isumrecl 12053*	The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z A e. RR )
Theorem	isumge0 12054*	An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ A )   =>    |- ( ph -> 0 <_ sum_ k e. Z A )
Theorem	isumadd 12055*	Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> seq M ( + , G ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z ( A + B ) = ( sum_ k e. Z A + sum_ k e. Z B ) )
Theorem	sumsplitdc 12056*	Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> ( A u. B ) C_ Z )   &    |- ( ( ph /\ k e. Z ) -> DECID k e. A )   &    |- ( ( ph /\ k e. Z ) -> DECID k e. B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , C , 0 ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = if ( k e. B , C , 0 ) )   &    |- ( ( ph /\ k e. ( A u. B ) ) -> C e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> seq M ( + , G ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. ( A u. B ) C = ( sum_ k e. A C + sum_ k e. B C ) )
Theorem	fsump1i 12057*	Optimized version of fsump1 12044 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- N = ( K + 1 )   &    |- ( k = N -> A = B )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> ( K e. Z /\ sum_ k e. ( M ... K ) A = S ) )   &    |- ( ph -> ( S + B ) = T )   =>    |- ( ph -> ( N e. Z /\ sum_ k e. ( M ... N ) A = T ) )
Theorem	fsum2dlemstep 12058*	Lemma for fsum2d 12059- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   &    |- ( ph -> -. y e. x )   &    |- ( ph -> ( x u. { y } ) C_ A )   &    |- ( ph -> x e. Fin )   &    |- ( ps <-> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D )   =>    |- ( ( ph /\ ps ) -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )
Theorem	fsum2d 12059*	Write a double sum as a sum over a two-dimensional region. Note that B ( j ) is a function of j. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D )
Theorem	fsumxp 12060*	Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. ( A X. B ) D )
Theorem	fsumcnv 12061*	Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014.)
|- ( x = <. j , k >. -> B = D )   &    |- ( y = <. k , j >. -> C = D )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> Rel A )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> sum_ x e. A B = sum_ y e. `' A C )
Theorem	fisumcom2 12062*	Interchange order of summation. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.) (Proof shortened by JJ, 2-Aug-2021.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ( ph /\ k e. C ) -> D e. Fin )   &    |- ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. C /\ j e. D ) ) )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> E e. CC )   =>    |- ( ph -> sum_ j e. A sum_ k e. B E = sum_ k e. C sum_ j e. D E )
Theorem	fsumcom 12063*	Interchange order of summation. (Contributed by NM, 15-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> sum_ j e. A sum_ k e. B C = sum_ k e. B sum_ j e. A C )
Theorem	fsum0diaglem 12064*	Lemma for fisum0diag 12065. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.)
|- ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( k e. ( 0 ... N ) /\ j e. ( 0 ... ( N - k ) ) ) )
Theorem	fisum0diag 12065*	Two ways to express "the sum of A ( j , k ) over the triangular region M <_ j, M <_ k, j + k <_ N". (Contributed by NM, 31-Dec-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.)
|- ( ( ph /\ ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) ) -> A e. CC )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) A = sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... ( N - k ) ) A )
Theorem	mptfzshft 12066*	1-1 onto function in maps-to notation which shifts a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) : ( ( M + K ) ... ( N + K ) ) -1-1-onto-> ( M ... N ) )
Theorem	fsumrev 12067*	Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( j = ( K - k ) -> A = B )   =>    |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( K - N ) ... ( K - M ) ) B )
Theorem	fsumshft 12068*	Index shift of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) (Proof shortened by AV, 8-Sep-2019.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( j = ( k - K ) -> A = B )   =>    |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )
Theorem	fsumshftm 12069*	Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( j = ( k + K ) -> A = B )   =>    |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M - K ) ... ( N - K ) ) B )
Theorem	fisumrev2 12070*	Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( j = ( ( M + N ) - k ) -> A = B )   =>    |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( M ... N ) B )
Theorem	fisum0diag2 12071*	Two ways to express "the sum of A ( j , k ) over the triangular region 0 <_ j, 0 <_ k, j + k <_ N". (Contributed by Mario Carneiro, 21-Jul-2014.)
|- ( x = k -> B = A )   &    |- ( x = ( k - j ) -> B = C )   &    |- ( ( ph /\ ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) ) -> A e. CC )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) A = sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... k ) C )
Theorem	fsummulc2 12072*	A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C e. CC )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( C x. sum_ k e. A B ) = sum_ k e. A ( C x. B ) )
Theorem	fsummulc1 12073*	A finite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C e. CC )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( sum_ k e. A B x. C ) = sum_ k e. A ( B x. C ) )
Theorem	fsumdivapc 12074*	A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C e. CC )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( sum_ k e. A B / C ) = sum_ k e. A ( B / C ) )
Theorem	fsumneg 12075*	Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> sum_ k e. A -u B = -u sum_ k e. A B )
Theorem	fsumsub 12076*	Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-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	fsum2mul 12077*	Separate the nested sum of the product C ( j ) x. D ( k ). (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ j e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. B ) -> D e. CC )   =>    |- ( ph -> sum_ j e. A sum_ k e. B ( C x. D ) = ( sum_ j e. A C x. sum_ k e. B D ) )
Theorem	fsumconst 12078*	The sum of constant terms ( k is not free in B). (Contributed by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ( A e. Fin /\ B e. CC ) -> sum_ k e. A B = ( (♯ ` A ) x. B ) )
Theorem	fsumdifsnconst 12079*	The sum of constant terms ( k is not free in C) over an index set excluding a singleton. (Contributed by AV, 7-Jan-2022.)
|- ( ( A e. Fin /\ B e. A /\ C e. CC ) -> sum_ k e. ( A \ { B } ) C = ( ( (♯ ` A ) - 1 ) x. C ) )
Theorem	modfsummodlem1 12080*	Lemma for modfsummod 12082. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
|- ( A. k e. ( A u. { z } ) B e. ZZ -> [_ z / k ]_ B e. ZZ )
Theorem	modfsummodlemstep 12081*	Induction step for modfsummod 12082. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.)
|- ( ph -> A e. Fin )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A. k e. ( A u. { z } ) B e. ZZ )   &    |- ( ph -> -. z e. A )   &    |- ( ph -> ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) )   =>    |- ( ph -> ( sum_ k e. ( A u. { z } ) B mod N ) = ( sum_ k e. ( A u. { z } ) ( B mod N ) mod N ) )
Theorem	modfsummod 12082*	A finite sum modulo a positive integer equals the finite sum of their summands modulo the positive integer, modulo the positive integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
|- ( ph -> N e. NN )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A. k e. A B e. ZZ )   =>    |- ( ph -> ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) )
Theorem	fsumge0 12083*	If all of the terms of a finite sum are nonnegative, so is the sum. (Contributed by NM, 26-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   =>    |- ( ph -> 0 <_ sum_ k e. A B )
Theorem	fsumlessfi 12084*	A shorter sum of nonnegative terms is no greater than a longer one. (Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon, 12-Oct-2022.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   &    |- ( ph -> C C_ A )   &    |- ( ph -> C e. Fin )   =>    |- ( ph -> sum_ k e. C B <_ sum_ k e. A B )
Theorem	fsumge1 12085*	A sum of nonnegative numbers is greater than or equal to any one of its terms. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 4-Jun-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   &    |- ( k = M -> B = C )   &    |- ( ph -> M e. A )   =>    |- ( ph -> C <_ sum_ k e. A B )
Theorem	fsum00 12086*	A sum of nonnegative numbers is zero iff all terms are zero. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   =>    |- ( ph -> ( sum_ k e. A B = 0 <-> A. k e. A B = 0 ) )
Theorem	fsumle 12087*	If all of the terms of finite sums compare, so do the sums. (Contributed by NM, 11-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> C e. RR )   &    |- ( ( ph /\ k e. A ) -> B <_ C )   =>    |- ( ph -> sum_ k e. A B <_ sum_ k e. A C )
Theorem	fsumlt 12088*	If every term in one finite sum is less than the corresponding term in another, then the first sum is less than the second. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> C e. RR )   &    |- ( ( ph /\ k e. A ) -> B < C )   =>    |- ( ph -> sum_ k e. A B < sum_ k e. A C )
Theorem	fsumabs 12089*	Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( abs ` sum_ k e. A B ) <_ sum_ k e. A ( abs ` B ) )
Theorem	telfsumo 12090*	Sum of a telescoping series, using half-open intervals. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( k = j -> A = B )   &    |- ( k = ( j + 1 ) -> A = C )   &    |- ( k = M -> A = D )   &    |- ( k = N -> A = E )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   =>    |- ( ph -> sum_ j e. ( M..^ N ) ( B - C ) = ( D - E ) )
Theorem	telfsumo2 12091*	Sum of a telescoping series. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( k = j -> A = B )   &    |- ( k = ( j + 1 ) -> A = C )   &    |- ( k = M -> A = D )   &    |- ( k = N -> A = E )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   =>    |- ( ph -> sum_ j e. ( M..^ N ) ( C - B ) = ( E - D ) )
Theorem	telfsum 12092*	Sum of a telescoping series. (Contributed by Scott Fenton, 24-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|- ( k = j -> A = B )   &    |- ( k = ( j + 1 ) -> A = C )   &    |- ( k = M -> A = D )   &    |- ( k = ( N + 1 ) -> A = E )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   =>    |- ( ph -> sum_ j e. ( M ... N ) ( B - C ) = ( D - E ) )
Theorem	telfsum2 12093*	Sum of a telescoping series. (Contributed by Mario Carneiro, 15-Jun-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|- ( k = j -> A = B )   &    |- ( k = ( j + 1 ) -> A = C )   &    |- ( k = M -> A = D )   &    |- ( k = ( N + 1 ) -> A = E )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   =>    |- ( ph -> sum_ j e. ( M ... N ) ( C - B ) = ( E - D ) )
Theorem	fsumparts 12094*	Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( k = j -> ( A = B /\ V = W ) )   &    |- ( k = ( j + 1 ) -> ( A = C /\ V = X ) )   &    |- ( k = M -> ( A = D /\ V = Y ) )   &    |- ( k = N -> ( A = E /\ V = Z ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> V e. CC )   =>    |- ( ph -> sum_ j e. ( M..^ N ) ( B x. ( X - W ) ) = ( ( ( E x. Z ) - ( D x. Y ) ) - sum_ j e. ( M..^ N ) ( ( C - B ) x. X ) ) )
Theorem	fsumrelem 12095*	Lemma for fsumre 12096, fsumim 12097, and fsumcj 12098. (Contributed by Mario Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- F : CC --> CC   &    |- ( ( x e. CC /\ y e. CC ) -> ( F ` ( x + y ) ) = ( ( F ` x ) + ( F ` y ) ) )   =>    |- ( ph -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) )
Theorem	fsumre 12096*	The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( Re ` sum_ k e. A B ) = sum_ k e. A ( Re ` B ) )
Theorem	fsumim 12097*	The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( Im ` sum_ k e. A B ) = sum_ k e. A ( Im ` B ) )
Theorem	fsumcj 12098*	The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( * ` sum_ k e. A B ) = sum_ k e. A ( * ` B ) )
Theorem	iserabs 12099*	Generalized triangle inequality: the absolute value of an infinite sum is less than or equal to the sum of absolute values. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Jim Kingdon, 14-Dec-2022.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ph -> seq M ( + , G ) ~~> B )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> ( abs ` A ) <_ B )
Theorem	cvgcmpub 12100*	An upper bound for the limit of a real infinite series. This theorem can also be used to compare two infinite series. (Contributed by Mario Carneiro, 24-Mar-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ph -> seq M ( + , G ) ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) <_ ( F ` k ) )   =>    |- ( ph -> B <_ A )