Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prod Structured version   Unicode version

Definition df-prod 27564
Description: Define the product of a series with an index set of integers  A. This definition takes most of the aspects of df-sum 13283 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a non-zero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.)
Assertion
Ref Expression
df-prod  |-  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 ) ) ) )
Distinct variable groups:    f, k, m, n, x, y    A, f, m, n, x, y    B, f, m, n, x, y
Allowed substitution hints:    A( k)    B( k)

Detailed syntax breakdown of Definition df-prod
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 vk . . 3  setvar  k
41, 2, 3cprod 27563 . 2  class  prod_ k  e.  A  B
5 vm . . . . . . . . 9  setvar  m
65cv 1369 . . . . . . . 8  class  m
7 cuz 10973 . . . . . . . 8  class  ZZ>=
86, 7cfv 5527 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 3437 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 vy . . . . . . . . . . 11  setvar  y
1110cv 1369 . . . . . . . . . 10  class  y
12 cc0 9394 . . . . . . . . . 10  class  0
1311, 12wne 2648 . . . . . . . . 9  wff  y  =/=  0
14 cmul 9399 . . . . . . . . . . 11  class  x.
15 cz 10758 . . . . . . . . . . . 12  class  ZZ
163cv 1369 . . . . . . . . . . . . . 14  class  k
1716, 1wcel 1758 . . . . . . . . . . . . 13  wff  k  e.  A
18 c1 9395 . . . . . . . . . . . . 13  class  1
1917, 2, 18cif 3900 . . . . . . . . . . . 12  class  if ( k  e.  A ,  B ,  1 )
203, 15, 19cmpt 4459 . . . . . . . . . . 11  class  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )
21 vn . . . . . . . . . . . 12  setvar  n
2221cv 1369 . . . . . . . . . . 11  class  n
2314, 20, 22cseq 11924 . . . . . . . . . 10  class  seq n
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )
24 cli 13081 . . . . . . . . . 10  class  ~~>
2523, 11, 24wbr 4401 . . . . . . . . 9  wff  seq n
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  y
2613, 25wa 369 . . . . . . . 8  wff  ( y  =/=  0  /\  seq n (  x.  , 
( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  y )
2726, 10wex 1587 . . . . . . 7  wff  E. y
( y  =/=  0  /\  seq n (  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  y )
2827, 21, 8wrex 2800 . . . . . 6  wff  E. n  e.  ( ZZ>= `  m ) E. y ( y  =/=  0  /\  seq n
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  y )
2914, 20, 6cseq 11924 . . . . . . 7  class  seq m
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )
30 vx . . . . . . . 8  setvar  x
3130cv 1369 . . . . . . 7  class  x
3229, 31, 24wbr 4401 . . . . . 6  wff  seq m
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  x
339, 28, 32w3a 965 . . . . 5  wff  ( 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 )
3433, 5, 15wrex 2800 . . . 4  wff  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 )
35 cfz 11555 . . . . . . . . 9  class  ...
3618, 6, 35co 6201 . . . . . . . 8  class  ( 1 ... m )
37 vf . . . . . . . . 9  setvar  f
3837cv 1369 . . . . . . . 8  class  f
3936, 1, 38wf1o 5526 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
40 cn 10434 . . . . . . . . . . 11  class  NN
4122, 38cfv 5527 . . . . . . . . . . . 12  class  ( f `
 n )
423, 41, 2csb 3396 . . . . . . . . . . 11  class  [_ (
f `  n )  /  k ]_ B
4321, 40, 42cmpt 4459 . . . . . . . . . 10  class  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
)
4414, 43, 18cseq 11924 . . . . . . . . 9  class  seq 1
(  x.  ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) )
456, 44cfv 5527 . . . . . . . 8  class  (  seq 1 (  x.  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m )
4631, 45wceq 1370 . . . . . . 7  wff  x  =  (  seq 1 (  x.  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
)
4739, 46wa 369 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  x.  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) )
4847, 37wex 1587 . . . . 5  wff  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  x.  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) )
4948, 5, 40wrex 2800 . . . 4  wff  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 ) )
5034, 49wo 368 . . 3  wff  ( 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 ) ) )
5150, 30cio 5488 . 2  class  ( 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 ) ) ) )
524, 51wceq 1370 1  wff  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 ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  prodex  27565  prodeq1f  27566  nfcprod1  27568  nfcprod  27569  prodeq2w  27570  prodeq2ii  27571  cbvprod  27573  zprod  27595  fprod  27599
  Copyright terms: Public domain W3C validator