P. 113 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11201-11300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sumsplitdc 11201*	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 11202*	Optimized version of fsump1 11189 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 11203*	Lemma for fsum2d 11204- 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 11204*	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 11205*	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 11206*	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 11207*	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 11208*	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 11209*	Lemma for fisum0diag 11210. (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 11210*	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 11211*	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 11212*	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 11213*	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 11214*	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 11215*	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 11216*	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 11217*	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 11218*	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 11219*	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 11220*	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 11221*	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 11222*	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 11223*	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 11224*	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 11225*	Lemma for modfsummod 11227. (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 11226*	Induction step for modfsummod 11227. (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 11227*	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 11228*	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 11229*	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 11230*	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 11231*	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 11232*	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 11233*	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 11234*	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 11235*	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 11236*	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 11237*	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 11238*	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 11239*	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 11240*	Lemma for fsumre 11241, fsumim 11242, and fsumcj 11243. (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 11241*	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 11242*	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 11243*	The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( * ` sum_ k e. A B ) = sum_ k e. A ( * ` B ) )
Theorem	iserabs 11244*	Generalized triangle inequality: the absolute value of an infinite sum is less than or equal to the sum of absolute values. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Jim Kingdon, 14-Dec-2022.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ph -> seq M ( + , G ) ~~> B )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> ( abs ` A ) <_ B )
Theorem	cvgcmpub 11245*	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	fsumiun 11246*	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 11247*	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	hash2iun 11248*	The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. Fin )   &    |- ( ( ph /\ x e. A /\ y e. B ) -> C e. Fin )   &    |- ( ph -> Disj x e. A U_ y e. B C )   &    |- ( ( ph /\ x e. A ) -> Disj y e. B C )   =>    |- ( ph -> (♯ ` U_ x e. A U_ y e. B C ) = sum_ x e. A sum_ y e. B (♯ ` C ) )
Theorem	hash2iun1dif1 11249*	The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.)
|- ( ph -> A e. Fin )   &    |- B = ( A \ { x } )   &    |- ( ( ph /\ x e. A /\ y e. B ) -> C e. Fin )   &    |- ( ph -> Disj x e. A U_ y e. B C )   &    |- ( ( ph /\ x e. A ) -> Disj y e. B C )   &    |- ( ( ph /\ x e. A /\ y e. B ) -> (♯ ` C ) = 1 )   =>    |- ( ph -> (♯ ` U_ x e. A U_ y e. B C ) = ( (♯ ` A ) x. ( (♯ ` A ) - 1 ) ) )
Theorem	hashrabrex 11250*	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 11251*	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 ) )
4.8.3  The binomial theorem
Theorem	binomlem 11252*	Lemma for binom 11253 (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 11253*	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 11252. 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 11254*	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 11255*	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 11256*	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 11257	Lemma for bcxmas 11258. (Contributed by Paul Chapman, 18-May-2007.)
|- ( A = B -> ( ( N + A ) _C A ) = ( ( N + B ) _C B ) )
Theorem	bcxmas 11258*	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 ) )
4.8.4  Infinite sums (cont.)
Theorem	isumshft 11259*	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 11260*	Split off the first N terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.)
|- 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 11261*	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 11262*	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 11263*	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 11264*	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	isumlessdc 11265*	A finite sum of nonnegative numbers is less than 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 -> A. k e. Z DECID k e. A )   &    |- ( ( 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 )
4.8.5  Miscellaneous converging and diverging sequences
Theorem	divcnv 11266*	The sequence of reciprocals of positive integers, multiplied by the factor A, converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Jim Kingdon, 22-Oct-2022.)
|- ( A e. CC -> ( n e. NN |-> ( A / n ) ) ~~> 0 )
4.8.6  Arithmetic series
Theorem	arisum 11267*	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 11268*	Arithmetic series sum of the first N nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 2-Aug-2021.)
|- ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
Theorem	trireciplem 11269	Lemma for trirecip 11270. 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 11270	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
4.8.7  Geometric series
Theorem	expcnvap0 11271*	A sequence of powers of a complex number A with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 23-Oct-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) < 1 )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
Theorem	expcnvre 11272*	A sequence of powers of a nonnegative real number less than one converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
Theorem	expcnv 11273*	A sequence of powers of a complex number A with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 28-Oct-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) < 1 )   =>    |- ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
Theorem	explecnv 11274*	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	geosergap 11275*	The value of the finite geometric series A ^ M + A ^ ( M + 1 ) +... + A ^ ( N - 1 ). (Contributed by Mario Carneiro, 2-May-2016.) (Revised by Jim Kingdon, 24-Oct-2022.)
|- ( 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	geoserap 11276*	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.) (Revised by Jim Kingdon, 24-Oct-2022.)
|- ( 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	pwm1geoserap1 11277*	The n-th power of a number decreased by 1 expressed by the finite geometric series 1 + A ^ 1 + A ^ 2 +... + A ^ ( N - 1 ). (Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon, 24-Oct-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A # 1 )   =>    |- ( ph -> ( ( A ^ N ) - 1 ) = ( ( A - 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) ) )
Theorem	absltap 11278	Less-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` A ) < B )   =>    |- ( ph -> A # B )
Theorem	absgtap 11279	Greater-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> B < ( abs ` A ) )   =>    |- ( ph -> A # B )
Theorem	geolim 11280*	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 ) ) )
Theorem	geolim2 11281*	The partial sums in the geometric series A ^ M + A ^ ( M + 1 )... converge to ( ( A ^ M ) / ( 1 - A ) ). (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) < 1 )   &    |- ( ph -> M e. NN0 )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( A ^ k ) )   =>    |- ( ph -> seq M ( + , F ) ~~> ( ( A ^ M ) / ( 1 - A ) ) )
Theorem	georeclim 11282*	The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> 1 < ( abs ` A ) )   &    |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( ( 1 / A ) ^ k ) )   =>    |- ( ph -> seq 0 ( + , F ) ~~> ( A / ( A - 1 ) ) )
Theorem	geo2sum 11283*	The value of the finite geometric series 2 ^ -u 1 + 2 ^ -u 2 +... + 2 ^ -u N, multiplied by a constant. (Contributed by Mario Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( N e. NN /\ A e. CC ) -> sum_ k e. ( 1 ... N ) ( A / ( 2 ^ k ) ) = ( A - ( A / ( 2 ^ N ) ) ) )
Theorem	geo2sum2 11284*	The value of the finite geometric series 1 + 2 + 4 + 8 +... + 2 ^ ( N - 1 ). (Contributed by Mario Carneiro, 7-Sep-2016.)
|- ( N e. NN0 -> sum_ k e. ( 0..^ N ) ( 2 ^ k ) = ( ( 2 ^ N ) - 1 ) )
Theorem	geo2lim 11285*	The value of the infinite geometric series 2 ^ -u 1 + 2 ^ -u 2 +... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014.)
|- F = ( k e. NN |-> ( A / ( 2 ^ k ) ) )   =>    |- ( A e. CC -> seq 1 ( + , F ) ~~> A )
Theorem	geoisum 11286*	The infinite sum of 1 + A ^ 1 + A ^ 2... is ( 1 / ( 1 - A ) ). (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN0 ( A ^ k ) = ( 1 / ( 1 - A ) ) )
Theorem	geoisumr 11287*	The infinite sum of reciprocals 1 + ( 1 / A ) ^ 1 + ( 1 / A ) ^ 2... is A / ( A - 1 ). (Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( A e. CC /\ 1 < ( abs ` A ) ) -> sum_ k e. NN0 ( ( 1 / A ) ^ k ) = ( A / ( A - 1 ) ) )
Theorem	geoisum1 11288*	The infinite sum of A ^ 1 + A ^ 2... is ( A / ( 1 - A ) ). (Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN ( A ^ k ) = ( A / ( 1 - A ) ) )
Theorem	geoisum1c 11289*	The infinite sum of A x. ( R ^ 1 ) + A x. ( R ^ 2 )... is ( A x. R ) / ( 1 - R ). (Contributed by NM, 2-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> sum_ k e. NN ( A x. ( R ^ k ) ) = ( ( A x. R ) / ( 1 - R ) ) )
Theorem	0.999... 11290	The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. 9 / 1 0 ^ 1 + 9 / 1 0 ^ 2 + 9 / 1 0 ^ 3 + ..., is exactly equal to 1. (Contributed by NM, 2-Nov-2007.) (Revised by AV, 8-Sep-2021.)
|- sum_ k e. NN ( 9 / (; 1 0 ^ k ) ) = 1
Theorem	geoihalfsum 11291	Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 11288. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 11290 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by AV, 9-Jul-2022.)
|- sum_ k e. NN ( 1 / ( 2 ^ k ) ) = 1
4.8.8  Ratio test for infinite series convergence
Theorem	cvgratnnlembern 11292	Lemma for cvgratnn 11300. Upper bound for a geometric progression of positive ratio less than one. (Contributed by Jim Kingdon, 24-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ph -> M e. NN )   =>    |- ( ph -> ( A ^ M ) < ( ( 1 / ( ( 1 / A ) - 1 ) ) / M ) )
Theorem	cvgratnnlemnexp 11293*	Lemma for cvgratnn 11300. (Contributed by Jim Kingdon, 15-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( abs ` ( F ` N ) ) <_ ( ( abs ` ( F ` 1 ) ) x. ( A ^ ( N - 1 ) ) ) )
Theorem	cvgratnnlemmn 11294*	Lemma for cvgratnn 11300. (Contributed by Jim Kingdon, 15-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( abs ` ( F ` N ) ) <_ ( ( abs ` ( F ` M ) ) x. ( A ^ ( N - M ) ) ) )
Theorem	cvgratnnlemseq 11295*	Lemma for cvgratnn 11300. (Contributed by Jim Kingdon, 21-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( ( seq 1 ( + , F ) ` N ) - ( seq 1 ( + , F ) ` M ) ) = sum_ i e. ( ( M + 1 ) ... N ) ( F ` i ) )
Theorem	cvgratnnlemabsle 11296*	Lemma for cvgratnn 11300. (Contributed by Jim Kingdon, 21-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( abs ` sum_ i e. ( ( M + 1 ) ... N ) ( F ` i ) ) <_ ( ( abs ` ( F ` M ) ) x. sum_ i e. ( ( M + 1 ) ... N ) ( A ^ ( i - M ) ) ) )
Theorem	cvgratnnlemsumlt 11297*	Lemma for cvgratnn 11300. (Contributed by Jim Kingdon, 23-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> sum_ i e. ( ( M + 1 ) ... N ) ( A ^ ( i - M ) ) < ( A / ( 1 - A ) ) )
Theorem	cvgratnnlemfm 11298*	Lemma for cvgratnn 11300. (Contributed by Jim Kingdon, 23-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   &    |- ( ph -> M e. NN )   =>    |- ( ph -> ( abs ` ( F ` M ) ) < ( ( ( ( 1 / ( ( 1 / A ) - 1 ) ) / A ) x. ( ( abs ` ( F ` 1 ) ) + 1 ) ) / M ) )
Theorem	cvgratnnlemrate 11299*	Lemma for cvgratnn 11300. (Contributed by Jim Kingdon, 21-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` N ) - ( seq 1 ( + , F ) ` M ) ) ) < ( ( ( ( ( 1 / ( ( 1 / A ) - 1 ) ) / A ) x. ( ( abs ` ( F ` 1 ) ) + 1 ) ) x. ( A / ( 1 - A ) ) ) / M ) )
Theorem	cvgratnn 11300*	Ratio test for convergence of a complex infinite series. If the ratio A of the absolute values of successive terms in an infinite sequence F is less than 1 for all terms, then the infinite sum of the terms of F converges to a complex number. Although this theorem is similar to cvgratz 11301 and cvgratgt0 11302, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 11119 is sensitive to how a sequence is indexed. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 12-Nov-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   =>    |- ( ph -> seq 1 ( + , F ) e. dom ~~> )