P. 119 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11801-11900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fz1f1o 11801*	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	nnf1o 11802	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 11803*	Lemma for sumrbdc 11805. (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 11804*	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 11805*	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 11806*	Lemma for summodc 11809. (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 11807*	Lemma for summodc 11809. (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 11808*	Lemma for summodc 11809. (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 11809*	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 11810*	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 11811*	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 11812*	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 11813*	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 11814	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 11815*	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 11816*	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 11817*	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 11818*	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 11819*	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 11820*	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 11821*	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 11822*	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 11823*	A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 11838 and fsump1 11846, which should make our notation clear and from which, along with closure fsumcl 11826, 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 11824*	- 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 11825*	- 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 11826*	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 11827*	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 11828*	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 11829*	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 11830*	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 11831*	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 11832*	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 11833*	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 11834*	Split a sum into two parts. A version of fsumsplit 11833 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 11835*	A sum of a singleton is the term. A version of sumsn 11837 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 11836*	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 11837*	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 11838*	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 11839*	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 11840*	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 11841*	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 11842*	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 11843*	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 11844*	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 11845*	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 11846*	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 11847*	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 11848*	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 11849*	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 11850*	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 11851*	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 11852*	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 11853*	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 11854*	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 11855*	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 11856*	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 11857*	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 11858*	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 11859*	Optimized version of fsump1 11846 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 11860*	Lemma for fsum2d 11861- 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 11861*	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 11862*	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 11863*	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 11864*	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 11865*	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 11866*	Lemma for fisum0diag 11867. (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 11867*	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 11868*	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 11869*	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 11870*	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 11871*	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 11872*	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 11873*	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 11874*	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 11875*	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 11876*	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 11877*	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 11878*	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 11879*	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 11880*	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 11881*	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 11882*	Lemma for modfsummod 11884. (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 11883*	Induction step for modfsummod 11884. (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 11884*	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 11885*	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 11886*	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 11887*	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 11888*	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 11889*	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 11890*	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 11891*	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 11892*	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 11893*	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 11894*	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 11895*	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 11896*	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 11897*	Lemma for fsumre 11898, fsumim 11899, and fsumcj 11900. (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 11898*	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 11899*	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 11900*	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 ) )