P. 120 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	explecnv 11901*	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 11902*	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 11903*	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 11904*	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 11905	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 11906	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 11907*	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 11908*	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 11909*	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 11910*	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 11911*	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 11912*	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 11913*	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 11914*	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 11915*	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 11916*	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... 11917	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 11918	Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 11915. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 11917 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 11919	Lemma for cvgratnn 11927. 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 11920*	Lemma for cvgratnn 11927. (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 11921*	Lemma for cvgratnn 11927. (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 11922*	Lemma for cvgratnn 11927. (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 11923*	Lemma for cvgratnn 11927. (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 11924*	Lemma for cvgratnn 11927. (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 11925*	Lemma for cvgratnn 11927. (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 11926*	Lemma for cvgratnn 11927. (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 11927*	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 11928 and cvgratgt0 11929, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 11746 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 11928*	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 11929*	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 11930*	Lemma for mertensabs 11933. 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 11931*	Lemma for mertensabs 11933. (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 11932*	Lemma for mertensabs 11933. (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 11933*	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 11934*	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 11935*	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 11936*	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 11937*	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 11938	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 11939	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 11940	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 11941*	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 11942*	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 11943*	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 11944*	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 11945*	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 11946	Extend class notation to include complex products.
class prod_ k e. A B
Definition	df-proddc 11947*	Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sumdc 11750 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 11948	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 11949*	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 11950*	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 11951*	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 11952*	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 11953*	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 11954*	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 11955*	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 11956*	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 11957*	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 11958*	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 11959*	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 11960*	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 11961*	Equality deduction for product. Note that unlike prodeq2dv 11962, 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 11962*	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 11963*	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 11964*	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 11965*	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 11966*	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 11967*	Lemma for prodrbdc 11970. (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 11968*	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 11969*	Lemma for prodrbdc 11970. (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 11970*	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 11971*	Lemma for prodmodc 11974. (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 11972*	Lemma for prodmodc 11974. (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 11973*	Lemma for prodmodc 11974. (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 11974*	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 11975*	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 11976*	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 11977*	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 11978*	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 11979*	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 11980*	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 11981	A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.)
|- prod_ k e. (/) A = 1
Theorem	prod1dc 11982*	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 11983*	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 11984*	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 11985*	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 )
Theorem	fprodssdc 11986*	Change the index set to a subset in a finite sum. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ph -> A. j e. B DECID j e. A )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 1 )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B C )
Theorem	fprodmul 11987*	The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   =>    |- ( ph -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) )
Theorem	prodsnf 11988*	A product of a singleton is the term. A version of prodsn 11989 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/_ k B   &    |- ( k = M -> A = B )   =>    |- ( ( M e. V /\ B e. CC ) -> prod_ k e. { M } A = B )
Theorem	prodsn 11989*	A product of a singleton is the term. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( k = M -> A = B )   =>    |- ( ( M e. V /\ B e. CC ) -> prod_ k e. { M } A = B )
Theorem	fprod1 11990*	A finite product of only one term is the term itself. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( k = M -> A = B )   =>    |- ( ( M e. ZZ /\ B e. CC ) -> prod_ k e. ( M ... M ) A = B )
Theorem	climprod1 11991	The limit of a product over one. (Contributed by Scott Fenton, 15-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )
Theorem	fprodsplitdc 11992*	Split a finite product into two parts. New proofs should use fprodsplit 11993 which is the same but with one fewer hypothesis. (Contributed by Scott Fenton, 16-Dec-2017.) (New usage is discouraged.)
|- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ph -> A. j e. U DECID j e. A )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )
Theorem	fprodsplit 11993*	Split a finite product into two parts. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )
Theorem	fprodm1 11994*	Separate out the last term in a finite product. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( k = N -> A = B )   =>    |- ( ph -> prod_ k e. ( M ... N ) A = ( prod_ k e. ( M ... ( N - 1 ) ) A x. B ) )
Theorem	fprod1p 11995*	Separate out the first term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( k = M -> A = B )   =>    |- ( ph -> prod_ k e. ( M ... N ) A = ( B x. prod_ k e. ( ( M + 1 ) ... N ) A ) )
Theorem	fprodp1 11996*	Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   &    |- ( k = ( N + 1 ) -> A = B )   =>    |- ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. B ) )
Theorem	fprodm1s 11997*	Separate out the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   =>    |- ( ph -> prod_ k e. ( M ... N ) A = ( prod_ k e. ( M ... ( N - 1 ) ) A x. [_ N / k ]_ A ) )
Theorem	fprodp1s 11998*	Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   =>    |- ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. [_ ( N + 1 ) / k ]_ A ) )
Theorem	prodsns 11999*	A product of the singleton is the term. (Contributed by Scott Fenton, 25-Dec-2017.)
|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> prod_ k e. { M } A = [_ M / k ]_ A )
Theorem	fprodunsn 12000*	Multiply in an additional term in a finite product. See also fprodsplitsn 12029 which is the same but with a F/ k ph hypothesis in place of the distinct variable condition between ph and k. (Contributed by Jim Kingdon, 16-Aug-2024.)
|- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( k = B -> C = D )   =>    |- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) )