P. 147 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	geolim 14601*	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 14602*	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 14603*	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 14604*	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 14605*	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 14606*	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	geomulcvg 14607*	The geometric series converges even if it is multiplied by k to result in the larger series k x. A ^ k. (Contributed by Mario Carneiro, 27-Mar-2015.)
|- F = ( k e. NN0 |-> ( k x. ( A ^ k ) ) )   =>    |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , F ) e. dom ~~> )
Theorem	geoisum 14608*	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 14609*	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 14610*	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 14611*	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... 14612	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, according to ZF set theory. Interestingly, about 40% of the people responding to a poll at http://forum.physorg.com/index.php?showtopic=13177 disagree. (Contributed by NM, 2-Nov-2007.) (Revised by AV, 8-Sep-2021.)
|- sum_ k e. NN ( 9 / (; 1 0 ^ k ) ) = 1
Theorem	0.999...OLD 14613	Obsolete version of 0.999... 14612 as of 8-Sep-2021. (Contributed by NM, 2-Nov-2007.) (New usage is discouraged.) (Proof modification is discouraged.)
|- sum_ k e. NN ( 9 / ( 10 ^ k ) ) = 1
Theorem	geoihalfsum 14614	Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 14610. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 14612 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.)
|- sum_ k e. NN ( 1 / ( 2 ^ k ) ) = 1
5.10.10  Ratio test for infinite series convergence
Theorem	cvgrat 14615*	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. Equivalent to first part of Exercise 4 of [Gleason] p. 182. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 27-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( 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 ~~> )
5.10.11  Mertens' theorem
Theorem	mertenslem1 14616*	Lemma for mertens 14618. (Contributed by Mario Carneiro, 29-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 -> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) )   &    |- ( ph -> ( 0 <_ sup ( T , RR , < ) /\ ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) ) )   =>    |- ( 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 14617*	Lemma for mertens 14618. (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	mertens 14618*	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.)
|- ( ( 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 ( + , H ) ~~> ( sum_ j e. NN0 A x. sum_ k e. NN0 B ) )
5.10.12  Finite and infinite products
5.10.12.1  Product sequences
Theorem	prodf 14619*	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 14620*	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	clim2div 14621*	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	prodfmul 14622*	The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( 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 14623	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 14624	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 14625	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	prodfn0 14626*	No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) =/= 0 )   =>    |- ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )
Theorem	prodfrec 14627*	The reciprocal of an infinite product. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) =/= 0 )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( 1 / ( F ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) )
Theorem	prodfdiv 14628*	The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) =/= 0 )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) / ( seq M ( x. , G ) ` N ) ) )
5.10.12.2  Non-trivial convergence
Theorem	ntrivcvg 14629*	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	ntrivcvgn0 14630*	A product that converges to a nonzero value 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 ) )
Theorem	ntrivcvgfvn0 14631*	Any value of a product sequence that converges to a nonzero value is itself nonzero. (Contributed by Scott Fenton, 20-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> seq M ( x. , F ) ~~> X )   &    |- ( ph -> X =/= 0 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )
Theorem	ntrivcvgtail 14632*	A tail of a non-trivially convergent sequence converges non-trivially. (Contributed by Scott Fenton, 20-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> seq M ( x. , F ) ~~> X )   &    |- ( ph -> X =/= 0 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> ( ( ~~> ` seq N ( x. , F ) ) =/= 0 /\ seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) )
Theorem	ntrivcvgmullem 14633*	Lemma for ntrivcvgmul 14634. (Contributed by Scott Fenton, 19-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> P e. Z )   &    |- ( ph -> X =/= 0 )   &    |- ( ph -> Y =/= 0 )   &    |- ( ph -> seq N ( x. , F ) ~~> X )   &    |- ( ph -> seq P ( x. , G ) ~~> Y )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ph -> N <_ P )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> E. q e. Z E. w ( w =/= 0 /\ seq q ( x. , H ) ~~> w ) )
Theorem	ntrivcvgmul 14634*	The product of two non-trivially converging products converges non-trivially. (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 -> E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) )
5.10.12.3  Complex products
Syntax	cprod 14635	Extend class notation to include complex products.
class prod_ k e. A B
Definition	df-prod 14636*	Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sum 14417 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.)
|- prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ 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 |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
Theorem	prodex 14637	A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.)
|- prod_ k e. A B e. _V
Theorem	prodeq1f 14638	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 14639*	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 14640*	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 14641*	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 14642*	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	prodeq2ii 14643*	Equality theorem for product, with the class expressions B and C guarded by _I to be always sets. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( A. k e. A ( _I ` B ) = ( _I ` C ) -> prod_ k e. A B = prod_ k e. A C )
Theorem	prodeq2 14644*	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 14645*	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 14646*	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 14647*	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 14648*	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 14649*	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 14650*	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 14651*	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 14652*	Equality deduction for product. Note that unlike prodeq2dv 14653, 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 14653*	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 14654*	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 14655*	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 14656*	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 14657*	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	prod2id 14658*	The second class argument to a product can be chosen so that it is always a set. (Contributed by Scott Fenton, 4-Dec-2017.)
|- prod_ k e. A B = prod_ k e. A ( _I ` B )
Theorem	prodrblem 14659*	Lemma for prodrb 14662. (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 -> N e. ( ZZ>= ` M ) )   =>    |- ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) = seq N ( x. , F ) )
Theorem	fprodcvg 14660*	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 -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> A C_ ( M ... N ) )   =>    |- ( ph -> seq M ( x. , F ) ~~> ( seq M ( x. , F ) ` N ) )
Theorem	prodrblem2 14661*	Lemma for prodrb 14662. (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 /\ N e. ( ZZ>= ` M ) ) -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )
Theorem	prodrb 14662*	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 -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )
Theorem	prodmolem3 14663*	Lemma for prodmo 14666. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )   &    |- H = ( j e. NN |-> [_ ( K ` j ) / k ]_ B )   &    |- ( 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	prodmolem2a 14664*	Lemma for prodmo 14666. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )   &    |- H = ( j e. NN |-> [_ ( K ` j ) / k ]_ B )   &    |- ( 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	prodmolem2 14665*	Lemma for prodmo 14666. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )   =>    |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ 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	prodmo 14666*	A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )   =>    |- ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ 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	zprod 14667*	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 /\ 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	iprod 14668*	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	zprodn0 14669*	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 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	iprodn0 14670*	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 )
5.10.12.4  Finite products
Theorem	fprod 14671*	The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.)
|- ( 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. , G ) ` M ) )
Theorem	fprodntriv 14672*	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 14673	A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.)
|- prod_ k e. (/) A = 1
Theorem	prod1 14674*	Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.)
|- ( ( A C_ ( ZZ>= ` M ) \/ A e. Fin ) -> prod_ k e. A 1 = 1 )
Theorem	prodfc 14675*	A lemma to facilitate conversions from the function form to the class-variable form of a product. (Contributed by Scott Fenton, 7-Dec-2017.)
|- prod_ j e. A ( ( k e. A |-> B ) ` j ) = prod_ k e. A B
Theorem	fprodf1o 14676*	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	prodss 14677*	Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.)
|- ( 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 /\ k e. ( B \ A ) ) -> C = 1 )   &    |- ( ph -> B C_ ( ZZ>= ` M ) )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B C )
Theorem	fprodss 14678*	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 /\ k e. ( B \ A ) ) -> C = 1 )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B C )
Theorem	fprodser 14679*	A finite product expressed in terms of a partial product of an infinite sequence. The recursive definition of a finite product follows from here. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   =>    |- ( ph -> prod_ k e. ( M ... N ) A = ( seq M ( x. , F ) ` N ) )
Theorem	fprodcl2lem 14680*	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> prod_ k e. A B e. S )
Theorem	fprodcllem 14681*	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> 1 e. S )   =>    |- ( ph -> prod_ k e. A B e. S )
Theorem	fprodcl 14682*	Closure of a finite product of complex numbers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> prod_ k e. A B e. CC )
Theorem	fprodrecl 14683*	Closure of a finite product of real numbers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   =>    |- ( ph -> prod_ k e. A B e. RR )
Theorem	fprodzcl 14684*	Closure of a finite product of integers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ZZ )   =>    |- ( ph -> prod_ k e. A B e. ZZ )
Theorem	fprodnncl 14685*	Closure of a finite product of positive integers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. NN )   =>    |- ( ph -> prod_ k e. A B e. NN )
Theorem	fprodrpcl 14686*	Closure of a finite product of positive reals. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR+ )   =>    |- ( ph -> prod_ k e. A B e. RR+ )
Theorem	fprodnn0cl 14687*	Closure of a finite product of nonnegative integers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. NN0 )   =>    |- ( ph -> prod_ k e. A B e. NN0 )
Theorem	fprodcllemf 14688*	Finite product closure lemma. A version of fprodcllem 14681 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> 1 e. S )   =>    |- ( ph -> prod_ k e. A B e. S )
Theorem	fprodreclf 14689*	Closure of a finite product of real numbers. A version of fprodrecl 14683 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   =>    |- ( ph -> prod_ k e. A B e. RR )
Theorem	fprodmul 14690*	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	fproddiv 14691*	The quotient of two finite products. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. A ) -> C =/= 0 )   =>    |- ( ph -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) )
Theorem	prodsn 14692*	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 14693*	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	prodsnf 14694*	A product of a singleton is the term. A version of prodsn 14692 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	climprod1 14695	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	fprodsplit 14696*	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 14697*	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 14698*	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 14699*	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 14700*	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 ) )