P. 123 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12201-12300   *Has distinct variable group(s)

Type	Label	Description
Statement
4.9.4  Infinite sums (cont.)
Theorem	isumshft 12201*	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 12202*	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 12203*	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 12204*	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 12205*	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 12206*	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 12207*	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 12208*	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 12209*	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 12210*	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 12211	Lemma for trirecip 12212. 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 12212	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 12213*	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 12214*	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 12215*	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 12216*	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 12217*	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 12218*	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 12219*	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 12220	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 12221	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 12222*	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 12223*	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 12224*	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 12225*	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 12226*	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 12227*	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 12228*	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 12229*	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 12230*	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 12231*	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... 12232	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 12233	Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 12230. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 12232 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 12234	Lemma for cvgratnn 12242. 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 12235*	Lemma for cvgratnn 12242. (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 12236*	Lemma for cvgratnn 12242. (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 12237*	Lemma for cvgratnn 12242. (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 12238*	Lemma for cvgratnn 12242. (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 12239*	Lemma for cvgratnn 12242. (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 12240*	Lemma for cvgratnn 12242. (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 12241*	Lemma for cvgratnn 12242. (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 12242*	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 12243 and cvgratgt0 12244, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 12060 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 12243*	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 12244*	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 12245*	Lemma for mertensabs 12248. 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 12246*	Lemma for mertensabs 12248. (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 12247*	Lemma for mertensabs 12248. (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 12248*	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 12249*	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 12250*	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 12251*	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 12252*	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 12253	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 12254	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 12255	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 12256*	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 12257*	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 12258*	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 12259*	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 12260*	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 12261	Extend class notation to include complex products.
class prod_ k e. A B
Definition	df-proddc 12262*	Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sumdc 12064 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 12263	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 12264*	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 12265*	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 12266*	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 12267*	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 12268*	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 12269*	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 12270*	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 12271*	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 12272*	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 12273*	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 12274*	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 12275*	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 12276*	Equality deduction for product. Note that unlike prodeq2dv 12277, 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 12277*	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 12278*	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 12279*	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 12280*	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 12281*	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 12282*	Lemma for prodrbdc 12285. (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 12283*	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 12284*	Lemma for prodrbdc 12285. (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 12285*	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 12286*	Lemma for prodmodc 12289. (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 12287*	Lemma for prodmodc 12289. (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 12288*	Lemma for prodmodc 12289. (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 12289*	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 12290*	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 12291*	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 12292*	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 12293*	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 12294*	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 12295*	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 12296	A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.)
|- prod_ k e. (/) A = 1
Theorem	prod1dc 12297*	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 12298*	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 12299*	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 12300*	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 )