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 25237
Description: Define the product of a series with an index set of integers  A. This definition takes most of the aspects of df-sum 12485 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  set  k
41, 2, 3cprod 25236 . 2  class  prod_ k  e.  A B
5 vm . . . . . . . . 9  set  m
65cv 1652 . . . . . . . 8  class  m
7 cuz 10493 . . . . . . . 8  class  ZZ>=
86, 7cfv 5457 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 3322 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 vy . . . . . . . . . . 11  set  y
1110cv 1652 . . . . . . . . . 10  class  y
12 cc0 8995 . . . . . . . . . 10  class  0
1311, 12wne 2601 . . . . . . . . 9  wff  y  =/=  0
14 cmul 9000 . . . . . . . . . . 11  class  x.
15 cz 10287 . . . . . . . . . . . 12  class  ZZ
163cv 1652 . . . . . . . . . . . . . 14  class  k
1716, 1wcel 1726 . . . . . . . . . . . . 13  wff  k  e.  A
18 c1 8996 . . . . . . . . . . . . 13  class  1
1917, 2, 18cif 3741 . . . . . . . . . . . 12  class  if ( k  e.  A ,  B ,  1 )
203, 15, 19cmpt 4269 . . . . . . . . . . 11  class  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )
21 vn . . . . . . . . . . . 12  set  n
2221cv 1652 . . . . . . . . . . 11  class  n
2314, 20, 22cseq 11328 . . . . . . . . . 10  class  seq  n
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )
24 cli 12283 . . . . . . . . . 10  class  ~~>
2523, 11, 24wbr 4215 . . . . . . . . 9  wff  seq  n
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  y
2613, 25wa 360 . . . . . . . 8  wff  ( y  =/=  0  /\  seq  n (  x.  , 
( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  y )
2726, 10wex 1551 . . . . . . 7  wff  E. y
( y  =/=  0  /\  seq  n (  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  y )
2827, 21, 8wrex 2708 . . . . . 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 11328 . . . . . . 7  class  seq  m
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )
30 vx . . . . . . . 8  set  x
3130cv 1652 . . . . . . 7  class  x
3229, 31, 24wbr 4215 . . . . . 6  wff  seq  m
(  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  x
339, 28, 32w3a 937 . . . . 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 2708 . . . 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 11048 . . . . . . . . 9  class  ...
3618, 6, 35co 6084 . . . . . . . 8  class  ( 1 ... m )
37 vf . . . . . . . . 9  set  f
3837cv 1652 . . . . . . . 8  class  f
3936, 1, 38wf1o 5456 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
40 cn 10005 . . . . . . . . . . 11  class  NN
4122, 38cfv 5457 . . . . . . . . . . . 12  class  ( f `
 n )
423, 41, 2csb 3253 . . . . . . . . . . 11  class  [_ (
f `  n )  /  k ]_ B
4321, 40, 42cmpt 4269 . . . . . . . . . 10  class  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
)
4414, 43, 18cseq 11328 . . . . . . . . 9  class  seq  1
(  x.  ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) )
456, 44cfv 5457 . . . . . . . 8  class  (  seq  1 (  x.  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m )
4631, 45wceq 1653 . . . . . . 7  wff  x  =  (  seq  1 (  x.  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
)
4739, 46wa 360 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  x.  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) )
4847, 37wex 1551 . . . . 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 2708 . . . 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 359 . . 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 5419 . 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 1653 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 set class
This definition is referenced by:  prodex  25238  prodeq1f  25239  nfcprod1  25241  nfcprod  25242  prodeq2w  25243  prodeq2ii  25244  cbvprod  25246  zprod  25268  fprod  25272
  Copyright terms: Public domain W3C validator