P. 121 of Theorem List - Intuitionistic Logic Explorer

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

Type	Label	Description
Statement
Theorem	fsumdivapc 12001*	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 12002*	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 12003*	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 12004*	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 12005*	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 12006*	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 12007*	Lemma for modfsummod 12009. (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 12008*	Induction step for modfsummod 12009. (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 12009*	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 12010*	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 12011*	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 12012*	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 12013*	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 12014*	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 12015*	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 12016*	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 12017*	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 12018*	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 12019*	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 12020*	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 12021*	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 12022*	Lemma for fsumre 12023, fsumim 12024, and fsumcj 12025. (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 12023*	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 12024*	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 12025*	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 12026*	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 12027*	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 12028*	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 12029*	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 12030*	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 12031*	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 12032*	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 12033*	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.9.3  The binomial theorem
Theorem	binomlem 12034*	Lemma for binom 12035 (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 12035*	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 12034. 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 12036*	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 12037*	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 12038*	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 12039	Lemma for bcxmas 12040. (Contributed by Paul Chapman, 18-May-2007.)
|- ( A = B -> ( ( N + A ) _C A ) = ( ( N + B ) _C B ) )
Theorem	bcxmas 12040*	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.9.4  Infinite sums (cont.)
Theorem	isumshft 12041*	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 12042*	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 12043*	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 12044*	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 12045*	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 12046*	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 12047*	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.9.5  Miscellaneous converging and diverging sequences
Theorem	divcnv 12048*	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.9.6  Arithmetic series
Theorem	arisum 12049*	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 12050*	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 12051	Lemma for trirecip 12052. 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 12052	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.9.7  Geometric series
Theorem	expcnvap0 12053*	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 12054*	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 12055*	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 12056*	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 12057*	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 12058*	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 12059*	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 12060	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 12061	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 12062*	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 12063*	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 12064*	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 12065*	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 12066*	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 12067*	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 12068*	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 12069*	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 12070*	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 12071*	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... 12072	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 12073	Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 12070. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 12072 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.9.8  Ratio test for infinite series convergence
Theorem	cvgratnnlembern 12074	Lemma for cvgratnn 12082. 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 12075*	Lemma for cvgratnn 12082. (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 12076*	Lemma for cvgratnn 12082. (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 12077*	Lemma for cvgratnn 12082. (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 12078*	Lemma for cvgratnn 12082. (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 12079*	Lemma for cvgratnn 12082. (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 12080*	Lemma for cvgratnn 12082. (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 12081*	Lemma for cvgratnn 12082. (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 12082*	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 12083 and cvgratgt0 12084, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 11901 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 ~~> )
Theorem	cvgratz 12083*	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. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   =>    |- ( ph -> seq M ( + , F ) e. dom ~~> )
Theorem	cvgratgt0 12084*	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 beyond some index B, then the infinite sum of the terms of F converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> 0 < A )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. W ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   =>    |- ( ph -> seq M ( + , F ) e. dom ~~> )
4.9.9  Mertens' theorem
Theorem	mertenslemub 12085*	Lemma for mertensabs 12088. An upper bound for T. (Contributed by Jim Kingdon, 3-Dec-2022.)
|- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. NN0 ) -> B e. CC )   &    |- ( ph -> seq 0 ( + , G ) e. dom ~~> )   &    |- T = { z | E. n e. ( 0 ... ( S - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }   &    |- ( ph -> X e. T )   &    |- ( ph -> S e. NN )   =>    |- ( ph -> X <_ sum_ n e. ( 0 ... ( S - 1 ) ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
Theorem	mertenslemi1 12086*	Lemma for mertensabs 12088. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|- ( ( ph /\ j e. NN0 ) -> ( F ` j ) = A )   &    |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )   &    |- ( ( ph /\ j e. NN0 ) -> A e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. NN0 ) -> B e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )   &    |- ( ph -> seq 0 ( + , K ) e. dom ~~> )   &    |- ( ph -> seq 0 ( + , G ) e. dom ~~> )   &    |- ( ph -> E e. RR+ )   &    |- T = { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }   &    |- ( ps <-> ( s e. NN /\ A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )   &    |- ( ph -> P e. RR )   &    |- ( ph -> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( P + 1 ) ) ) ) )   &    |- ( ph -> 0 <_ P )   &    |- ( ph -> A. w e. T w <_ P )   =>    |- ( ph -> E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
Theorem	mertenslem2 12087*	Lemma for mertensabs 12088. (Contributed by Mario Carneiro, 28-Apr-2014.)
|- ( ( ph /\ j e. NN0 ) -> ( F ` j ) = A )   &    |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )   &    |- ( ( ph /\ j e. NN0 ) -> A e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. NN0 ) -> B e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )   &    |- ( ph -> seq 0 ( + , K ) e. dom ~~> )   &    |- ( ph -> seq 0 ( + , G ) e. dom ~~> )   &    |- ( ph -> E e. RR+ )   &    |- T = { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }   &    |- ( ps <-> ( s e. NN /\ A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )   =>    |- ( ph -> E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
Theorem	mertensabs 12088*	Mertens' theorem. If A ( j ) is an absolutely convergent series and B ( k ) is convergent, then ( sum_ j e. NN0 A ( j ) x. sum_ k e. NN0 B ( k ) ) = sum_ k e. NN0 sum_ j e. ( 0 ... k ) ( A ( j ) x. B ( k - j ) ) (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 8-Dec-2022.)
|- ( ( ph /\ j e. NN0 ) -> ( F ` j ) = A )   &    |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )   &    |- ( ( ph /\ j e. NN0 ) -> A e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. NN0 ) -> B e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )   &    |- ( ph -> seq 0 ( + , K ) e. dom ~~> )   &    |- ( ph -> seq 0 ( + , G ) e. dom ~~> )   &    |- ( ph -> seq 0 ( + , F ) e. dom ~~> )   =>    |- ( ph -> seq 0 ( + , H ) ~~> ( sum_ j e. NN0 A x. sum_ k e. NN0 B ) )
4.9.10  Finite and infinite products
4.9.10.1  Product sequences
Theorem	prodf 12089*	An infinite product of complex terms is a function from an upper set of integers to CC. (Contributed by Scott Fenton, 4-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> seq M ( x. , F ) : Z --> CC )
Theorem	clim2prod 12090*	The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> seq ( N + 1 ) ( x. , F ) ~~> A )   =>    |- ( ph -> seq M ( x. , F ) ~~> ( ( seq M ( x. , F ) ` N ) x. A ) )
Theorem	clim2divap 12091*	The limit of an infinite product with an initial segment removed. (Contributed by Scott Fenton, 20-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> seq M ( x. , F ) ~~> A )   &    |- ( ph -> ( seq M ( x. , F ) ` N ) # 0 )   =>    |- ( ph -> seq ( N + 1 ) ( x. , F ) ~~> ( A / ( seq M ( x. , F ) ` N ) ) )
Theorem	prod3fmul 12092*	The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) x. ( seq M ( x. , G ) ` N ) ) )
Theorem	prodf1 12093	The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> ( seq M ( x. , ( Z X. { 1 } ) ) ` N ) = 1 )
Theorem	prodf1f 12094	A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) = ( Z X. { 1 } ) )
Theorem	prodfclim1 12095	The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )
Theorem	prodfap0 12096*	The product of finitely many terms apart from zero is apart from zero. (Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon, 23-Mar-2024.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) # 0 )   =>    |- ( ph -> ( seq M ( x. , F ) ` N ) # 0 )
Theorem	prodfrecap 12097*	The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) # 0 )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( 1 / ( F ` k ) ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )   =>    |- ( ph -> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) )
Theorem	prodfdivap 12098*	The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) # 0 )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) / ( seq M ( x. , G ) ` N ) ) )
4.9.10.2  Non-trivial convergence
Theorem	ntrivcvgap 12099*	A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> E. n e. Z E. y ( y # 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> seq M ( x. , F ) e. dom ~~> )
Theorem	ntrivcvgap0 12100*	A product that converges to a value apart from zero converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> seq M ( x. , F ) ~~> X )   &    |- ( ph -> X # 0 )   =>    |- ( ph -> E. n e. Z E. y ( y # 0 /\ seq n ( x. , F ) ~~> y ) )