HomeHome Intuitionistic Logic Explorer
Theorem List (p. 116 of 142)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 11501-11600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
4.8.10  Finite and infinite products
 
4.8.10.1  Product sequences
 
Theoremprodf 11501* 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 )
 
Theoremclim2prod 11502* 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 ) )
 
Theoremclim2divap 11503* 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 ) ) )
 
Theoremprod3fmul 11504* 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 ) ) )
 
Theoremprodf1 11505 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 )
 
Theoremprodf1f 11506 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 } ) )
 
Theoremprodfclim1 11507 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 )
 
Theoremprodfap0 11508* 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 )
 
Theoremprodfrecap 11509* 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 ) ) )
 
Theoremprodfdivap 11510* 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.8.10.2  Non-trivial convergence
 
Theoremntrivcvgap 11511* 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  ~~>  )
 
Theoremntrivcvgap0 11512* 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.8.10.3  Complex products
 
Syntaxcprod 11513 Extend class notation to include complex products.
 class  prod_ k  e.  A  B
 
Definitiondf-proddc 11514* Define the product of a series with an index set of integers  A. This definition takes most of the aspects of df-sumdc 11317 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 ) ) ) )
 
Theoremprodeq1f 11515 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 )
 
Theoremprodeq1 11516* Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
 |-  ( A  =  B  -> 
 prod_ k  e.  A  C  =  prod_ k  e.  B  C )
 
Theoremnfcprod1 11517* Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F/_ k A   =>    |-  F/_ k prod_ k  e.  A  B
 
Theoremnfcprod 11518* 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
 
Theoremprodeq2w 11519* 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 )
 
Theoremprodeq2 11520* 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 )
 
Theoremcbvprod 11521* 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
 
Theoremcbvprodv 11522* 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
 
Theoremcbvprodi 11523* 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
 
Theoremprodeq1i 11524* Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  A  =  B   =>    |-  prod_ k  e.  A  C  =  prod_ k  e.  B  C
 
Theoremprodeq2i 11525* 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
 
Theoremprodeq12i 11526* 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
 
Theoremprodeq1d 11527* 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 )
 
Theoremprodeq2d 11528* Equality deduction for product. Note that unlike prodeq2dv 11529, 
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 )
 
Theoremprodeq2dv 11529* 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 )
 
Theoremprodeq2sdv 11530* 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 )
 
Theorem2cprodeq2dv 11531* 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 )
 
Theoremprodeq12dv 11532* 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 )
 
Theoremprodeq12rdv 11533* 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 )
 
Theoremprodrbdclem 11534* Lemma for prodrbdc 11537. (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 ) )
 
Theoremfproddccvg 11535* 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 ) )
 
Theoremprodrbdclem2 11536* Lemma for prodrbdc 11537. (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 )
 )
 
Theoremprodrbdc 11537* 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 )
 )
 
Theoremprodmodclem3 11538* Lemma for prodmodc 11541. (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 ) )
 
Theoremprodmodclem2a 11539* Lemma for prodmodc 11541. (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 ) )
 
Theoremprodmodclem2 11540* Lemma for prodmodc 11541. (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 )
 )
 
Theoremprodmodc 11541* 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 ) ) ) )
 
Theoremzproddc 11542* 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 ) ) )
 
Theoremiprodap 11543* 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 ) ) )
 
Theoremzprodap0 11544* 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 )
 
Theoremiprodap0 11545* 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.8.10.4  Finite products
 
Theoremfprodseq 11546* 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 ) )
 
Theoremfprodntrivap 11547* 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 )
 )
 
Theoremprod0 11548 A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.)
 |- 
 prod_ k  e.  (/)  A  =  1
 
Theoremprod1dc 11549* 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 )
 
Theoremprodfct 11550* 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 )
 
Theoremfprodf1o 11551* 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 )
 
Theoremprodssdc 11552* 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 )
 
Theoremfprodssdc 11553* 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 )
 
Theoremfprodmul 11554* 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 ) )
 
Theoremprodsnf 11555* A product of a singleton is the term. A version of prodsn 11556 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 )
 
Theoremprodsn 11556* 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 )
 
Theoremfprod1 11557* 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 )
 
Theoremclimprod1 11558 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 )
 
Theoremfprodsplitdc 11559* Split a finite product into two parts. New proofs should use fprodsplit 11560 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 ) )
 
Theoremfprodsplit 11560* 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 ) )
 
Theoremfprodm1 11561* 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 ) )
 
Theoremfprod1p 11562* 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 ) )
 
Theoremfprodp1 11563* 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 ) )
 
Theoremfprodm1s 11564* 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 ) )
 
Theoremfprodp1s 11565* 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 ) )
 
Theoremprodsns 11566* 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 )
 
Theoremfprodunsn 11567* Multiply in an additional term in a finite product. See also fprodsplitsn 11596 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 ) )
 
Theoremfprodcl2lem 11568* Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
 |-  ( 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 )
 
Theoremfprodcllem 11569* 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 )
 
Theoremfprodcl 11570* 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 )
 
Theoremfprodrecl 11571* 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 )
 
Theoremfprodzcl 11572* 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 )
 
Theoremfprodnncl 11573* 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 )
 
Theoremfprodrpcl 11574* 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+ )
 
Theoremfprodnn0cl 11575* 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 )
 
Theoremfprodcllemf 11576* Finite product closure lemma. A version of fprodcllem 11569 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 )
 
Theoremfprodreclf 11577* Closure of a finite product of real numbers. A version of fprodrecl 11571 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 )
 
Theoremfprodfac 11578* Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017.)
 |-  ( A  e.  NN0  ->  ( ! `  A )  =  prod_ k  e.  (
 1 ... A ) k )
 
Theoremfprodabs 11579* The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  A  e.  CC )   =>    |-  ( ph  ->  ( abs `  prod_ k  e.  ( M ... N ) A )  =  prod_ k  e.  ( M ... N ) ( abs `  A ) )
 
Theoremfprodeq0 11580* Any finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  A  e.  CC )   &    |-  ( ( ph  /\  k  =  N ) 
 ->  A  =  0 )   =>    |-  ( ( ph  /\  K  e.  ( ZZ>= `  N )
 )  ->  prod_ k  e.  ( M ... K ) A  =  0
 )
 
Theoremfprodshft 11581* Shift the index of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.)
 |-  ( ph  ->  K  e.  ZZ )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ZZ )   &    |-  ( ( ph  /\  j  e.  ( M ... N ) )  ->  A  e.  CC )   &    |-  ( j  =  ( k  -  K )  ->  A  =  B )   =>    |-  ( ph  ->  prod_ j  e.  ( M ... N ) A  =  prod_ k  e.  ( ( M  +  K ) ... ( N  +  K ) ) B )
 
Theoremfprodrev 11582* Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.)
 |-  ( ph  ->  K  e.  ZZ )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ZZ )   &    |-  ( ( ph  /\  j  e.  ( M ... N ) )  ->  A  e.  CC )   &    |-  ( j  =  ( K  -  k
 )  ->  A  =  B )   =>    |-  ( ph  ->  prod_ j  e.  ( M ... N ) A  =  prod_ k  e.  ( ( K  -  N ) ... ( K  -  M ) ) B )
 
Theoremfprodconst 11583* The product of constant terms ( k is not free in  B). (Contributed by Scott Fenton, 12-Jan-2018.)
 |-  ( ( A  e.  Fin  /\  B  e.  CC )  -> 
 prod_ k  e.  A  B  =  ( B ^ ( `  A )
 ) )
 
Theoremfprodap0 11584* A finite product of nonzero terms is nonzero. (Contributed by Scott Fenton, 15-Jan-2018.)
 |-  ( ph  ->  A  e.  Fin )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B #  0 )   =>    |-  ( ph  ->  prod_ k  e.  A  B #  0 )
 
Theoremfprod2dlemstep 11585* Lemma for fprod2d 11586- induction step. (Contributed by Scott Fenton, 30-Jan-2018.)
 |-  ( z  =  <. j ,  k >.  ->  D  =  C )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  (
 ( ph  /\  j  e.  A )  ->  B  e.  Fin )   &    |-  ( ( ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  C  e.  CC )   &    |-  ( ph  ->  -.  y  e.  x )   &    |-  ( ph  ->  ( x  u.  { y } )  C_  A )   &    |-  ( ph  ->  x  e.  Fin )   &    |-  ( ps 
 <-> 
 prod_ j  e.  x  prod_ k  e.  B  C  =  prod_ z  e.  U_  j  e.  x  ( { j }  X.  B ) D )   =>    |-  ( ( ph  /\  ps )  ->  prod_ j  e.  ( x  u.  { y }
 ) prod_ k  e.  B  C  =  prod_ z  e.  U_  j  e.  ( x  u.  { y }
 ) ( { j }  X.  B ) D )
 
Theoremfprod2d 11586* Write a double product as a product over a two-dimensional region. Compare fsum2d 11398. (Contributed by Scott Fenton, 30-Jan-2018.)
 |-  ( z  =  <. j ,  k >.  ->  D  =  C )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  (
 ( ph  /\  j  e.  A )  ->  B  e.  Fin )   &    |-  ( ( ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  C  e.  CC )   =>    |-  ( ph  ->  prod_ j  e.  A  prod_ k  e.  B  C  =  prod_ z  e.  U_  j  e.  A  ( { j }  X.  B ) D )
 
Theoremfprodxp 11587* Combine two products into a single product over the cartesian product. (Contributed by Scott Fenton, 1-Feb-2018.)
 |-  ( z  =  <. j ,  k >.  ->  D  =  C )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  B  e.  Fin )   &    |-  ( ( ph  /\  (
 j  e.  A  /\  k  e.  B )
 )  ->  C  e.  CC )   =>    |-  ( ph  ->  prod_ j  e.  A  prod_ k  e.  B  C  =  prod_ z  e.  ( A  X.  B ) D )
 
Theoremfprodcnv 11588* Transform a product region using the converse operation. (Contributed by Scott Fenton, 1-Feb-2018.)
 |-  ( x  =  <. j ,  k >.  ->  B  =  D )   &    |-  ( y  = 
 <. k ,  j >.  ->  C  =  D )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  Rel  A )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  CC )   =>    |-  ( ph  ->  prod_ x  e.  A  B  =  prod_ y  e.  `'  A C )
 
Theoremfprodcom2fi 11589* Interchange order of multiplication. Note that  B ( j ) and  D ( k ) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018.) (Proof shortened by JJ, 2-Aug-2021.)
 |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  C  e.  Fin )   &    |-  (
 ( ph  /\  j  e.  A )  ->  B  e.  Fin )   &    |-  ( ( ph  /\  k  e.  C ) 
 ->  D  e.  Fin )   &    |-  ( ph  ->  ( ( j  e.  A  /\  k  e.  B )  <->  ( k  e.  C  /\  j  e.  D ) ) )   &    |-  ( ( ph  /\  (
 j  e.  A  /\  k  e.  B )
 )  ->  E  e.  CC )   =>    |-  ( ph  ->  prod_ j  e.  A  prod_ k  e.  B  E  =  prod_ k  e.  C  prod_ j  e.  D  E )
 
Theoremfprodcom 11590* Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018.)
 |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  B  e.  Fin )   &    |-  (
 ( ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  C  e.  CC )   =>    |-  ( ph  ->  prod_ j  e.  A  prod_ k  e.  B  C  =  prod_ k  e.  B  prod_ j  e.  A  C )
 
Theoremfprod0diagfz 11591* Two ways to express "the product of  A ( j ,  k ) over the triangular region  M  <_  j,  M  <_  k,  j  +  k  <_  N. Compare fisum0diag 11404. (Contributed by Scott Fenton, 2-Feb-2018.)
 |-  ( ( ph  /\  (
 j  e.  ( 0
 ... N )  /\  k  e.  ( 0 ... ( N  -  j
 ) ) ) ) 
 ->  A  e.  CC )   &    |-  ( ph  ->  N  e.  ZZ )   =>    |-  ( ph  ->  prod_ j  e.  ( 0 ... N ) prod_ k  e.  (
 0 ... ( N  -  j ) ) A  =  prod_ k  e.  (
 0 ... N ) prod_
 j  e.  ( 0
 ... ( N  -  k ) ) A )
 
Theoremfprodrec 11592* The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
 |-  ( ph  ->  A  e.  Fin )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B #  0 )   =>    |-  ( ph  ->  prod_ k  e.  A  ( 1  /  B )  =  (
 1  /  prod_ k  e.  A  B ) )
 
Theoremfproddivap 11593* 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 ) )
 
Theoremfproddivapf 11594* The quotient of two finite products. A version of fproddivap 11593 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.  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 ) )
 
Theoremfprodsplitf 11595* Split a finite product into two parts. A version of fprodsplit 11560 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |- 
 F/ k ph   &    |-  ( 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 ) )
 
Theoremfprodsplitsn 11596* Separate out a term in a finite product. See also fprodunsn 11567 which is the same but with a distinct variable condition in place of  F/ k ph. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |- 
 F/ k ph   &    |-  F/_ k D   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  B  e.  V )   &    |-  ( ph  ->  -.  B  e.  A )   &    |-  ( ( ph  /\  k  e.  A )  ->  C  e.  CC )   &    |-  ( k  =  B  ->  C  =  D )   &    |-  ( ph  ->  D  e.  CC )   =>    |-  ( ph  ->  prod_
 k  e.  ( A  u.  { B }
 ) C  =  (
 prod_ k  e.  A  C  x.  D ) )
 
Theoremfprodsplit1f 11597* Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |- 
 F/ k ph   &    |-  ( ph  ->  F/_ k D )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  A )   &    |-  (
 ( ph  /\  k  =  C )  ->  B  =  D )   =>    |-  ( ph  ->  prod_ k  e.  A  B  =  ( D  x.  prod_ k  e.  ( A  \  { C } ) B ) )
 
Theoremfprodclf 11598* Closure of a finite product of complex numbers. A version of fprodcl 11570 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.  CC )   =>    |-  ( ph  ->  prod_ k  e.  A  B  e.  CC )
 
Theoremfprodap0f 11599* A finite product of terms apart from zero is apart from zero. A version of fprodap0 11584 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
 |- 
 F/ k ph   &    |-  ( ph  ->  A  e.  Fin )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B #  0 )   =>    |-  ( ph  ->  prod_
 k  e.  A  B #  0 )
 
Theoremfprodge0 11600* If all the terms of a finite product are nonnegative, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |- 
 F/ k ph   &    |-  ( ph  ->  A  e.  Fin )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B  e.  RR )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  0  <_  B )   =>    |-  ( ph  ->  0  <_  prod_
 k  e.  A  B )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14113
  Copyright terms: Public domain < Previous  Next >