MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sum Unicode version

Definition df-sum 12206
Description: Define the sum of a series with an index set of integers  A.  k is normally a free variable in  B, i.e.  B can be thought of as  B ( k ). This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers) by summo 12237. Examples:  sum_ k  e. 
{ 1 ,  2 ,  4 }  k means  1  +  2  + 
4  =  7, and  sum_ k  e.  NN  ( 1  / 
( 2 ^ k
) )  =  1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 12385). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
Assertion
Ref Expression
df-sum  |-  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) ) ) )
Distinct variable groups:    f, k, m, n, x    A, f, m, n, x    B, f, m, n, x
Allowed substitution hints:    A( k)    B( k)

Detailed syntax breakdown of Definition df-sum
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 vk . . 3  set  k
41, 2, 3csu 12205 . 2  class  sum_ k  e.  A  B
5 vm . . . . . . . . 9  set  m
65cv 1632 . . . . . . . 8  class  m
7 cuz 10277 . . . . . . . 8  class  ZZ>=
86, 7cfv 5292 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 3186 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 caddc 8785 . . . . . . . 8  class  +
11 cz 10071 . . . . . . . . 9  class  ZZ
123cv 1632 . . . . . . . . . . 11  class  k
1312, 1wcel 1701 . . . . . . . . . 10  wff  k  e.  A
14 cc0 8782 . . . . . . . . . 10  class  0
1513, 2, 14cif 3599 . . . . . . . . 9  class  if ( k  e.  A ,  B ,  0 )
163, 11, 15cmpt 4114 . . . . . . . 8  class  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) )
1710, 16, 6cseq 11093 . . . . . . 7  class  seq  m
(  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )
18 vx . . . . . . . 8  set  x
1918cv 1632 . . . . . . 7  class  x
20 cli 12005 . . . . . . 7  class  ~~>
2117, 19, 20wbr 4060 . . . . . 6  wff  seq  m
(  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x
229, 21wa 358 . . . . 5  wff  ( A 
C_  ( ZZ>= `  m
)  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )
2322, 5, 11wrex 2578 . . . 4  wff  E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )
24 c1 8783 . . . . . . . . 9  class  1
25 cfz 10829 . . . . . . . . 9  class  ...
2624, 6, 25co 5900 . . . . . . . 8  class  ( 1 ... m )
27 vf . . . . . . . . 9  set  f
2827cv 1632 . . . . . . . 8  class  f
2926, 1, 28wf1o 5291 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
30 vn . . . . . . . . . . 11  set  n
31 cn 9791 . . . . . . . . . . 11  class  NN
3230cv 1632 . . . . . . . . . . . . 13  class  n
3332, 28cfv 5292 . . . . . . . . . . . 12  class  ( f `
 n )
343, 33, 2csb 3115 . . . . . . . . . . 11  class  [_ (
f `  n )  /  k ]_ B
3530, 31, 34cmpt 4114 . . . . . . . . . 10  class  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
)
3610, 35, 24cseq 11093 . . . . . . . . 9  class  seq  1
(  +  ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) )
376, 36cfv 5292 . . . . . . . 8  class  (  seq  1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m )
3819, 37wceq 1633 . . . . . . 7  wff  x  =  (  seq  1 (  +  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
)
3929, 38wa 358 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  +  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) )
4039, 27wex 1532 . . . . 5  wff  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) )
4140, 5, 31wrex 2578 . . . 4  wff  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) )
4223, 41wo 357 . . 3  wff  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) ) )
4342, 18cio 5254 . 2  class  ( iota
x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq  1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) ) ) )
444, 43wceq 1633 1  wff  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  sumex  12207  sumeq1f  12208  nfsum1  12210  nfsum  12211  sumeq2w  12212  sumeq2ii  12213  cbvsum  12215  zsum  12238  fsum  12240
  Copyright terms: Public domain W3C validator