P. 119 of Theorem List - Intuitionistic Logic Explorer

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

Type	Label	Description
Statement
4.9.4  Infinite sums (cont.)
Theorem	isumshft 11801*	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 11802*	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 11803*	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 11804*	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 11805*	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 11806*	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 11807*	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 11808*	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 11809*	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 11810*	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 11811	Lemma for trirecip 11812. 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 11812	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 11813*	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 11814*	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 11815*	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 11816*	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 11817*	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 11818*	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 11819*	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 11820	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 11821	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 11822*	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 11823*	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 11824*	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 11825*	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 11826*	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 11827*	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 11828*	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 11829*	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 11830*	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 11831*	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... 11832	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 11833	Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 11830. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 11832 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 11834	Lemma for cvgratnn 11842. 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 11835*	Lemma for cvgratnn 11842. (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 11836*	Lemma for cvgratnn 11842. (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 11837*	Lemma for cvgratnn 11842. (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 11838*	Lemma for cvgratnn 11842. (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 11839*	Lemma for cvgratnn 11842. (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 11840*	Lemma for cvgratnn 11842. (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 11841*	Lemma for cvgratnn 11842. (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 11842*	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 11843 and cvgratgt0 11844, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 11661 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 11843*	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 11844*	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 11845*	Lemma for mertensabs 11848. 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 11846*	Lemma for mertensabs 11848. (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 11847*	Lemma for mertensabs 11848. (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 11848*	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 11849*	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 11850*	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 11851*	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 11852*	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 11853	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 11854	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 11855	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 11856*	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 11857*	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 11858*	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 11859*	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 11860*	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 ) )
4.9.10.3  Complex products
Syntax	cprod 11861	Extend class notation to include complex products.
class prod_ k e. A B
Definition	df-proddc 11862*	Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sumdc 11665 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 21-Mar-2024.)
|- prod_ k e. A B = ( iota x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
Theorem	prodeq1f 11863	Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
|- F/_ k A   &    |- F/_ k B   =>    |- ( A = B -> prod_ k e. A C = prod_ k e. B C )
Theorem	prodeq1 11864*	Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
|- ( A = B -> prod_ k e. A C = prod_ k e. B C )
Theorem	nfcprod1 11865*	Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F/_ k A   =>    |- F/_ k prod_ k e. A B
Theorem	nfcprod 11866*	Bound-variable hypothesis builder for product: if x is (effectively) not free in A and B, it is not free in prod_ k e. A B. (Contributed by Scott Fenton, 1-Dec-2017.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x prod_ k e. A B
Theorem	prodeq2w 11867*	Equality theorem for product, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( A. k B = C -> prod_ k e. A B = prod_ k e. A C )
Theorem	prodeq2 11868*	Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( A. k e. A B = C -> prod_ k e. A B = prod_ k e. A C )
Theorem	cbvprod 11869*	Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( j = k -> B = C )   &    |- F/_ k A   &    |- F/_ j A   &    |- F/_ k B   &    |- F/_ j C   =>    |- prod_ j e. A B = prod_ k e. A C
Theorem	cbvprodv 11870*	Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( j = k -> B = C )   =>    |- prod_ j e. A B = prod_ k e. A C
Theorem	cbvprodi 11871*	Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F/_ k B   &    |- F/_ j C   &    |- ( j = k -> B = C )   =>    |- prod_ j e. A B = prod_ k e. A C
Theorem	prodeq1i 11872*	Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- A = B   =>    |- prod_ k e. A C = prod_ k e. B C
Theorem	prodeq2i 11873*	Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( k e. A -> B = C )   =>    |- prod_ k e. A B = prod_ k e. A C
Theorem	prodeq12i 11874*	Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- A = B   &    |- ( k e. A -> C = D )   =>    |- prod_ k e. A C = prod_ k e. B D
Theorem	prodeq1d 11875*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B C )
Theorem	prodeq2d 11876*	Equality deduction for product. Note that unlike prodeq2dv 11877, k may occur in ph. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( ph -> A. k e. A B = C )   =>    |- ( ph -> prod_ k e. A B = prod_ k e. A C )
Theorem	prodeq2dv 11877*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( ( ph /\ k e. A ) -> B = C )   =>    |- ( ph -> prod_ k e. A B = prod_ k e. A C )
Theorem	prodeq2sdv 11878*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( ph -> B = C )   =>    |- ( ph -> prod_ k e. A B = prod_ k e. A C )
Theorem	2cprodeq2dv 11879*	Equality deduction for double product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( ( ph /\ j e. A /\ k e. B ) -> C = D )   =>    |- ( ph -> prod_ j e. A prod_ k e. B C = prod_ j e. A prod_ k e. B D )
Theorem	prodeq12dv 11880*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( ph -> A = B )   &    |- ( ( ph /\ k e. A ) -> C = D )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B D )
Theorem	prodeq12rdv 11881*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( ph -> A = B )   &    |- ( ( ph /\ k e. B ) -> C = D )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B D )
Theorem	prodrbdclem 11882*	Lemma for prodrbdc 11885. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) = seq N ( x. , F ) )
Theorem	fproddccvg 11883*	The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> seq M ( x. , F ) ~~> ( seq M ( x. , F ) ` N ) )
Theorem	prodrbdclem2 11884*	Lemma for prodrbdc 11885. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ph -> A C_ ( ZZ>= ` N ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> DECID k e. A )   =>    |- ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )
Theorem	prodrbdc 11885*	Rebase the starting point of a product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ph -> A C_ ( ZZ>= ` N ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> DECID k e. A )   =>    |- ( ph -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )
Theorem	prodmodclem3 11886*	Lemma for prodmodc 11889. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( f ` j ) / k ]_ B , 1 ) )   &    |- H = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( K ` j ) / k ]_ B , 1 ) )   &    |- ( ph -> ( M e. NN /\ N e. NN ) )   &    |- ( ph -> f : ( 1 ... M ) -1-1-onto-> A )   &    |- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )   =>    |- ( ph -> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , H ) ` N ) )
Theorem	prodmodclem2a 11887*	Lemma for prodmodc 11889. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( f ` j ) / k ]_ B , 1 ) )   &    |- H = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( K ` j ) / k ]_ B , 1 ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ph -> f : ( 1 ... N ) -1-1-onto-> A )   &    |- ( ph -> K Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )   =>    |- ( ph -> seq M ( x. , F ) ~~> ( seq 1 ( x. , G ) ` N ) )
Theorem	prodmodclem2 11888*	Lemma for prodmodc 11889. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( f ` j ) / k ]_ B , 1 ) )   =>    |- ( ( ph /\ E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )
Theorem	prodmodc 11889*	A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.) (Modified by Jim Kingdon, 14-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( f ` j ) / k ]_ B , 1 ) )   =>    |- ( ph -> E* x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) )
Theorem	zproddc 11890*	Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. n e. Z E. y ( y # 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ph -> A C_ Z )   &    |- ( ph -> A. j e. Z DECID j e. A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> prod_ k e. A B = ( ~~> ` seq M ( x. , F ) ) )
Theorem	iprodap 11891*	Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. n e. Z E. y ( y # 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> prod_ k e. Z B = ( ~~> ` seq M ( x. , F ) ) )
Theorem	zprodap0 11892*	Nonzero series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 6-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> X # 0 )   &    |- ( ph -> seq M ( x. , F ) ~~> X )   &    |- ( ph -> A. j e. Z DECID j e. A )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> prod_ k e. A B = X )
Theorem	iprodap0 11893*	Nonzero series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> X # 0 )   &    |- ( ph -> seq M ( x. , F ) ~~> X )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> prod_ k e. Z B = X )
4.9.10.4  Finite products
Theorem	fprodseq 11894*	The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
|- ( k = ( F ` n ) -> B = C )   &    |- ( ph -> M e. NN )   &    |- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )   =>    |- ( ph -> prod_ k e. A B = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )
Theorem	fprodntrivap 11895*	A non-triviality lemma for finite sequences. (Contributed by Scott Fenton, 16-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> E. n e. Z E. y ( y # 0 /\ seq n ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )
Theorem	prod0 11896	A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.)
|- prod_ k e. (/) A = 1
Theorem	prod1dc 11897*	Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.)
|- ( ( ( M e. ZZ /\ A C_ ( ZZ>= ` M ) /\ A. j e. ( ZZ>= ` M )DECID j e. A ) \/ A e. Fin ) -> prod_ k e. A 1 = 1 )
Theorem	prodfct 11898*	A lemma to facilitate conversions from the function form to the class-variable form of a product. (Contributed by Scott Fenton, 7-Dec-2017.)
|- ( A. k e. A B e. CC -> prod_ j e. A ( ( k e. A |-> B ) ` j ) = prod_ k e. A B )
Theorem	fprodf1o 11899*	Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017.)
|- ( k = G -> B = D )   &    |- ( ph -> C e. Fin )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ( ph /\ n e. C ) -> ( F ` n ) = G )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> prod_ k e. A B = prod_ n e. C D )
Theorem	prodssdc 11900*	Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon, 6-Aug-2024.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ph -> E. n e. ( ZZ>= ` M ) E. y ( y # 0 /\ seq n ( x. , ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ) ~~> y ) )   &    |- ( ph -> A. j e. ( ZZ>= ` M )DECID j e. A )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 1 )   &    |- ( ph -> B C_ ( ZZ>= ` M ) )   &    |- ( ph -> A. j e. ( ZZ>= ` M )DECID j e. B )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B C )