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	nfsum 12101	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 12102*	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 12103*	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 12104	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 12105*	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 12106*	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 12107*	Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|- A = B   =>    |- sum_ k e. A C = sum_ k e. B C
Theorem	sumeq2i 12108*	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 12109*	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 12110*	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 12111*	Equality deduction for sum. Note that unlike sumeq2dv 12112, 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 12112*	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 12113*	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 12114*	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 12115*	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 12116*	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 12117*	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 12118*	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 12119*	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 12120*	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 12121	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 12122*	Lemma for sumrbdc 12124. (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 12123*	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 12124*	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 12125*	Lemma for summodc 12128. (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 12126*	Lemma for summodc 12128. (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 12127*	Lemma for summodc 12128. (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 12128*	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 12129*	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 12130*	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 12131*	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 12132*	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 12133	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 12134*	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 12135*	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 12136*	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 12137*	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 12138*	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 12139*	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 12140*	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 12141*	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 12142*	A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 12157 and fsump1 12165, which should make our notation clear and from which, along with closure fsumcl 12145, 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 12143*	- 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 12144*	- 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 12145*	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 12146*	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 12147*	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 12148*	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 12149*	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 12150*	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 12151*	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 12152*	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 12153*	Split a sum into two parts. A version of fsumsplit 12152 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 12154*	A sum of a singleton is the term. A version of sumsn 12156 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 12155*	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 12156*	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 12157*	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 12158*	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 12159*	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 12160*	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 12161*	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 12162*	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 12163*	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 12164*	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 12165*	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 12166*	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 12167*	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 12168*	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 12169*	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 12170*	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 12171*	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 12172*	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 12173*	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 12174*	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 12175*	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 12176*	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 12177*	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 12178*	Optimized version of fsump1 12165 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 12179*	Lemma for fsum2d 12180- 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 12180*	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 12181*	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 12182*	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 12183*	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 12184*	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 12185*	Lemma for fisum0diag 12186. (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 12186*	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 12187*	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 12188*	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 12189*	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 12190*	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 12191*	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 12192*	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 12193*	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 12194*	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 12195*	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 12196*	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 12197*	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 12198*	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 12199*	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 12200*	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 ) )