P. 137 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13601-13700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isumrecl 13601*	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 13602*	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 13603*	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	sumsplit 13604*	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 ) -> ( 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 13605*	Optimized version of fsump1 13592 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	fsum2dlem 13606*	Lemma for fsum2d 13607- induction step. (Contributed by Mario Carneiro, 23-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 -> -. y e. x )   &    |- ( ph -> ( x u. { y } ) C_ A )   &    |- ( 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 13607*	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 13608*	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 13609*	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	fsumcom2 13610*	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.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C e. Fin )   &    |- ( ( ph /\ j e. A ) -> B 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 13611*	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 13612*	Lemma for fsum0diag 13613. (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	fsum0diag 13613*	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 -> 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 13614*	1-1 onto function in maps-to notation which shifts a finite set of sequential integers. Formerly part of proof for fsumshft 13616. (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 13615*	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 13616*	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 13617*	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	fsumrev2 13618*	Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.)
|- ( ( 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	fsum0diag2 13619*	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 -> 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 13620*	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 13621*	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	fsumdivc 13622*	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 13623*	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 13624*	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 13625*	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 13626*	The sum of constant terms ( k is not free in A). (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	modfsummodslem1 13627*	Lemma 1 for modfsummods 13628. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
|- ( A. k e. ( A u. { z } ) B e. ZZ -> [_ z / k ]_ B e. ZZ )
Theorem	modfsummods 13628*	Induction step for modfsummod 13629. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
|- ( ( A e. Fin /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) -> ( ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) -> ( sum_ k e. ( A u. { z } ) B mod N ) = ( sum_ k e. ( A u. { z } ) ( B mod N ) mod N ) ) )
Theorem	modfsummod 13629*	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 13630*	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	fsumless 13631*	A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by NM, 26-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 ) -> 0 <_ B )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> sum_ k e. C B <_ sum_ k e. A B )
Theorem	fsumge1 13632*	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 13633*	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 13634*	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 13635*	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 13636*	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 13637*	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 13638*	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 13639*	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 13640*	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 13641*	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 13642*	Lemma for fsumre 13643, fsumim 13644, and fsumcj 13645. (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 13643*	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 13644*	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 13645*	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	fsumrlim 13646*	Limit of a finite sum of converging sequences. Note that C ( k ) is a collection of functions with implicit parameter k, each of which converges to D ( k ) as n ~~> +oo. (Contributed by Mario Carneiro, 22-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )   &    |- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) ~~> r D )   =>    |- ( ph -> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D )
Theorem	fsumo1 13647*	The finite sum of eventually bounded functions (where the index set B does not depend on x) is eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 22-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )   &    |- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> sum_ k e. B C ) e. O(1) )
Theorem	o1fsum 13648*	If A ( k ) is O(1), then sum_ k <_ x , A ( k ) is O( x). (Contributed by Mario Carneiro, 23-May-2016.)
|- ( ( ph /\ k e. NN ) -> A e. V )   &    |- ( ph -> ( k e. NN |-> A ) e. O(1) )   =>    |- ( ph -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) e. O(1) )
Theorem	seqabs 13649*	Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by Mario Carneiro, 26-Mar-2014.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> ( abs ` ( seq M ( + , F ) ` N ) ) <_ ( seq M ( + , G ) ` N ) )
Theorem	iserabs 13650*	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 Mario Carneiro, 27-May-2014.)
|- 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	cvgcmp 13651*	A comparison test for convergence of a real infinite series. Exercise 3 of [Gleason] p. 182. (Contributed by NM, 1-May-2005.) (Revised 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 ) e. dom ~~> )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 <_ ( G ` k ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( G ` k ) <_ ( F ` k ) )   =>    |- ( ph -> seq M ( + , G ) e. dom ~~> )
Theorem	cvgcmpub 13652*	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 )
Theorem	cvgcmpce 13653*	A comparison test for convergence of a complex infinite series. (Contributed by NM, 25-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( abs ` ( G ` k ) ) <_ ( C x. ( F ` k ) ) )   =>    |- ( ph -> seq M ( + , G ) e. dom ~~> )
Theorem	abscvgcvg 13654*	An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( abs ` ( G ` k ) ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> seq M ( + , G ) e. dom ~~> )
Theorem	climfsum 13655*	Limit of a finite sum of converging sequences. Note that F ( k ) is a collection of functions with implicit parameter k, each of which converges to B ( k ) as n ~~> +oo. (Contributed by Mario Carneiro, 22-Jul-2014.) (Proof shortened by Mario Carneiro, 22-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> F ~~> B )   &    |- ( ph -> H e. W )   &    |- ( ( ph /\ ( k e. A /\ n e. Z ) ) -> ( F ` n ) e. CC )   &    |- ( ( ph /\ n e. Z ) -> ( H ` n ) = sum_ k e. A ( F ` n ) )   =>    |- ( ph -> H ~~> sum_ k e. A B )
Theorem	fsumiun 13656*	Sum over a disjoint indexed union. (Contributed by Mario Carneiro, 1-Jul-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. Fin )   &    |- ( ph -> Disj x e. A B )   &    |- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> sum_ k e. U_ x e. A B C = sum_ x e. A sum_ k e. B C )
Theorem	hashiun 13657*	The cardinality of a disjoint indexed union. (Contributed by Mario Carneiro, 24-Jan-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. Fin )   &    |- ( ph -> Disj x e. A B )   =>    |- ( ph -> ( # ` U_ x e. A B ) = sum_ x e. A ( # ` B ) )
Theorem	hashrabrex 13658*	The number of elements in a class abstraction with a restricted existential quantification. (Contributed by Alexander van der Vekens, 29-Jul-2018.)
|- ( ph -> Y e. Fin )   &    |- ( ( ph /\ y e. Y ) -> { x e. X | ps } e. Fin )   &    |- ( ph -> Disj y e. Y { x e. X | ps } )   =>    |- ( ph -> ( # ` { x e. X | E. y e. Y ps } ) = sum_ y e. Y ( # ` { x e. X | ps } ) )
Theorem	hashuni 13659*	The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- ( ph -> A e. Fin )   &    |- ( ph -> A C_ Fin )   &    |- ( ph -> Disj x e. A x )   =>    |- ( ph -> ( # ` U. A ) = sum_ x e. A ( # ` x ) )
Theorem	qshash 13660*	The cardinality of a set with an equivalence relation is the sum of the cardinalities of its equivalence classes. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( ph -> .~ Er A )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> ( # ` A ) = sum_ x e. ( A /. .~ ) ( # ` x ) )
Theorem	ackbijnn 13661*	Translate the Ackermann bijection ackbij1 8549 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- F = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ y e. x ( 2 ^ y ) )   =>    |- F : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0
5.10.4  The binomial theorem
Theorem	binomlem 13662*	Lemma for binom 13663 (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ps -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( A + B ) ^ ( N + 1 ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
Theorem	binom 13663*	The binomial theorem: ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ). Theorem 15-2.8 of [Gleason] p. 296. This part of the proof sets up the induction and does the base case, with the bulk of the work (the induction step) in binomlem 13662. This is Metamath 100 proof #44. (Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )
Theorem	binom1p 13664*	Special case of the binomial theorem for ( 1 + A ) ^ N. (Contributed by Paul Chapman, 10-May-2007.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( 1 + A ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( A ^ k ) ) )
Theorem	binom11 13665*	Special case of the binomial theorem for 2 ^ N. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( N e. NN0 -> ( 2 ^ N ) = sum_ k e. ( 0 ... N ) ( N _C k ) )
Theorem	binom1dif 13666*	A summation for the difference between ( ( A + 1 ) ^ N ) and ( A ^ N ). (Contributed by Scott Fenton, 9-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( ( A + 1 ) ^ N ) - ( A ^ N ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) )
Theorem	bcxmaslem1 13667	Lemma for bcxmas 13668. (Contributed by Paul Chapman, 18-May-2007.)
|- ( A = B -> ( ( N + A ) _C A ) = ( ( N + B ) _C B ) )
Theorem	bcxmas 13668*	Parallel summation (Christmas Stocking) theorem for Pascal's Triangle. (Contributed by Paul Chapman, 18-May-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( N + 1 ) + M ) _C M ) = sum_ j e. ( 0 ... M ) ( ( N + j ) _C j ) )
5.10.5  The inclusion/exclusion principle
Theorem	incexclem 13669*	Lemma for incexc 13670. (Contributed by Mario Carneiro, 7-Aug-2017.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` B ) - ( # ` ( B i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( B i^i |^| s ) ) ) )
Theorem	incexc 13670*	The inclusion/exclusion principle for counting the elements of a finite union of finite sets. This is Metamath 100 proof #96. (Contributed by Mario Carneiro, 7-Aug-2017.)
|- ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
Theorem	incexc2 13671*	The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.)
|- ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ n e. ( 1 ... ( # ` A ) ) ( ( -u 1 ^ ( n - 1 ) ) x. sum_ s e. { k e. ~P A | ( # ` k ) = n } ( # ` |^| s ) ) )
5.10.6  Infinite sums (cont.)
Theorem	isumshft 13672*	Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` ( M + K ) )   &    |- ( j = ( K + k ) -> A = B )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ j e. W ) -> A e. CC )   =>    |- ( ph -> sum_ j e. W A = sum_ k e. Z B )
Theorem	isumsplit 13673*	Split off the first N terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> N e. Z )   &    |- ( ( 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 = ( sum_ k e. ( M ... ( N - 1 ) ) A + sum_ k e. W A ) )
Theorem	isum1p 13674*	The infinite sum of a converging infinite series equals the first term plus the infinite sum of the rest of it. (Contributed by NM, 2-Jan-2006.) (Revised 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. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z A = ( ( F ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) A ) )
Theorem	isumnn0nn 13675*	Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( k = 0 -> A = B )   &    |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. NN0 ) -> A e. CC )   &    |- ( ph -> seq 0 ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. NN0 A = ( B + sum_ k e. NN A ) )
Theorem	isumrpcl 13676*	The infinite sum of positive reals is positive. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR+ )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. W A e. RR+ )
Theorem	isumle 13677*	Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007.) (Revised 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 /\ k e. Z ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. RR )   &    |- ( ( ph /\ k e. Z ) -> A <_ B )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> seq M ( + , G ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z A <_ sum_ k e. Z B )
Theorem	isumless 13678*	A finite sum of nonnegative numbers is less or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ B )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. A B <_ sum_ k e. Z B )
Theorem	isumsup2 13679*	An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014.)
|- Z = ( ZZ>= ` M )   &    |- G = seq M ( + , F )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ A )   &    |- ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )   =>    |- ( ph -> G ~~> sup ( ran G , RR , < ) )
Theorem	isumsup 13680*	An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014.)
|- Z = ( ZZ>= ` M )   &    |- G = seq M ( + , F )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ A )   &    |- ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )   =>    |- ( ph -> sum_ k e. Z A = sup ( ran G , RR , < ) )
Theorem	isumltss 13681*	A partial sum of a series with positive terms is less than the infinite sum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. RR+ )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. A B < sum_ k e. Z B )
Theorem	climcndslem1 13682*	Lemma for climcnds 13684: bound the original series by the condensed series. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( F ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )   =>    |- ( ( ph /\ N e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) )
Theorem	climcndslem2 13683*	Lemma for climcnds 13684: bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( F ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )   =>    |- ( ( ph /\ N e. NN ) -> ( seq 1 ( + , G ) ` N ) <_ ( 2 x. ( seq 1 ( + , F ) ` ( 2 ^ N ) ) ) )
Theorem	climcnds 13684*	The Cauchy condensation test. If a ( k ) is a decreasing sequence of nonnegative terms, then sum_ k e. NN a ( k ) converges iff sum_ n e. NN0 2 ^ n x. a ( 2 ^ n ) converges. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( F ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )   =>    |- ( ph -> ( seq 1 ( + , F ) e. dom ~~> <-> seq 0 ( + , G ) e. dom ~~> ) )
5.10.7  Miscellaneous converging and diverging sequences
Theorem	divrcnv 13685*	The sequence of reciprocals of real numbers, multiplied by the factor A, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. CC -> ( n e. RR+ |-> ( A / n ) ) ~~> r 0 )
Theorem	divcnv 13686*	The sequence of reciprocals of positive integers, multiplied by the factor A, converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 18-Sep-2014.)
|- ( A e. CC -> ( n e. NN |-> ( A / n ) ) ~~> 0 )
Theorem	flo1 13687	The floor function satisfies |_ ( x ) = x + O(1). (Contributed by Mario Carneiro, 21-May-2016.)
|- ( x e. RR |-> ( x - ( |_ ` x ) ) ) e. O(1)
Theorem	supcvg 13688*	Extract a sequence f in X such that the image of the points in the bounded set A converges to the supremum S of the set. Similar to Equation 4 of [Kreyszig] p. 144. The proof uses countable choice ax-cc 8746. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
|- X e. _V   &    |- S = sup ( A , RR , < )   &    |- R = ( n e. NN |-> ( S - ( 1 / n ) ) )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> F : X -onto-> A )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   =>    |- ( ph -> E. f ( f : NN --> X /\ ( F o. f ) ~~> S ) )
Theorem	infcvgaux1i 13689*	Auxiliary theorem for applications of supcvg 13688. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.)
|- R = { x | E. y e. X x = -u A }   &    |- ( y e. X -> A e. RR )   &    |- Z e. X   &    |- E. z e. RR A. w e. R w <_ z   =>    |- ( R C_ RR /\ R =/= (/) /\ E. z e. RR A. w e. R w <_ z )
Theorem	infcvgaux2i 13690*	Auxiliary theorem for applications of supcvg 13688. (Contributed by NM, 4-Mar-2008.)
|- R = { x | E. y e. X x = -u A }   &    |- ( y e. X -> A e. RR )   &    |- Z e. X   &    |- E. z e. RR A. w e. R w <_ z   &    |- S = -u sup ( R , RR , < )   &    |- ( y = C -> A = B )   =>    |- ( C e. X -> S <_ B )
Theorem	harmonic 13691	The harmonic series H diverges. This fact follows from the stronger emcl 23468, which establishes that the harmonic series grows as log n + gamma + o(1), but this uses a more elementary method, attributed to Nicole Oresme (1323-1382). This is Metamath 100 proof #34. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- F = ( n e. NN |-> ( 1 / n ) )   &    |- H = seq 1 ( + , F )   =>    |- -. H e. dom ~~>
5.10.8  Arithmetic series
Theorem	arisum 13692*	Arithmetic series sum of the first N positive integers. This is Metamath 100 proof #68. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 22-May-2014.)
|- ( N e. NN0 -> sum_ k e. ( 1 ... N ) k = ( ( ( N ^ 2 ) + N ) / 2 ) )
Theorem	arisum2 13693*	Arithmetic series sum of the first N nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
Theorem	trireciplem 13694	Lemma for trirecip 13695. Show that the sum converges. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|- F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )   =>    |- seq 1 ( + , F ) ~~> 1
Theorem	trirecip 13695	The sum of the reciprocals of the triangle numbers converge to two. This is Metamath 100 proof #42. (Contributed by Scott Fenton, 23-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|- sum_ k e. NN ( 2 / ( k x. ( k + 1 ) ) ) = 2
5.10.9  Geometric series
Theorem	expcnv 13696*	A sequence of powers of a complex number A with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) < 1 )   =>    |- ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
Theorem	explecnv 13697*	A sequence of terms converges to zero when it is less than powers of a number A whose absolute value is smaller than 1. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> ( abs ` A ) < 1 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( abs ` ( F ` k ) ) <_ ( A ^ k ) )   =>    |- ( ph -> F ~~> 0 )
Theorem	geoserg 13698*	The value of the finite geometric series A ^ M + A ^ ( M + 1 ) +... + A ^ ( N - 1 ). (Contributed by Mario Carneiro, 2-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 1 )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> sum_ k e. ( M..^ N ) ( A ^ k ) = ( ( ( A ^ M ) - ( A ^ N ) ) / ( 1 - A ) ) )
Theorem	geoser 13699*	The value of the finite geometric series 1 + A ^ 1 + A ^ 2 +... + A ^ ( N - 1 ). This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Proof shortened by Mario Carneiro, 15-Jun-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 1 )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) )
Theorem	geolim 13700*	The partial sums in the infinite series 1 + A ^ 1 + A ^ 2... converge to ( 1 / ( 1 - A ) ). (Contributed by NM, 15-May-2006.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) < 1 )   &    |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( A ^ k ) )   =>    |- ( ph -> seq 0 ( + , F ) ~~> ( 1 / ( 1 - A ) ) )