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

Definition df-sum 12511
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 12542. 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 12690). (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 12510 . 2  class  sum_ k  e.  A  B
5 vm . . . . . . . . 9  set  m
65cv 1652 . . . . . . . 8  class  m
7 cuz 10519 . . . . . . . 8  class  ZZ>=
86, 7cfv 5483 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 3306 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 caddc 9024 . . . . . . . 8  class  +
11 cz 10313 . . . . . . . . 9  class  ZZ
123cv 1652 . . . . . . . . . . 11  class  k
1312, 1wcel 1727 . . . . . . . . . 10  wff  k  e.  A
14 cc0 9021 . . . . . . . . . 10  class  0
1513, 2, 14cif 3763 . . . . . . . . 9  class  if ( k  e.  A ,  B ,  0 )
163, 11, 15cmpt 4291 . . . . . . . 8  class  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) )
1710, 16, 6cseq 11354 . . . . . . 7  class  seq  m
(  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )
18 vx . . . . . . . 8  set  x
1918cv 1652 . . . . . . 7  class  x
20 cli 12309 . . . . . . 7  class  ~~>
2117, 19, 20wbr 4237 . . . . . 6  wff  seq  m
(  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x
229, 21wa 360 . . . . 5  wff  ( A 
C_  ( ZZ>= `  m
)  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )
2322, 5, 11wrex 2712 . . . 4  wff  E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )
24 c1 9022 . . . . . . . . 9  class  1
25 cfz 11074 . . . . . . . . 9  class  ...
2624, 6, 25co 6110 . . . . . . . 8  class  ( 1 ... m )
27 vf . . . . . . . . 9  set  f
2827cv 1652 . . . . . . . 8  class  f
2926, 1, 28wf1o 5482 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
30 vn . . . . . . . . . . 11  set  n
31 cn 10031 . . . . . . . . . . 11  class  NN
3230cv 1652 . . . . . . . . . . . . 13  class  n
3332, 28cfv 5483 . . . . . . . . . . . 12  class  ( f `
 n )
343, 33, 2csb 3267 . . . . . . . . . . 11  class  [_ (
f `  n )  /  k ]_ B
3530, 31, 34cmpt 4291 . . . . . . . . . 10  class  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
)
3610, 35, 24cseq 11354 . . . . . . . . 9  class  seq  1
(  +  ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) )
376, 36cfv 5483 . . . . . . . 8  class  (  seq  1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m )
3819, 37wceq 1653 . . . . . . 7  wff  x  =  (  seq  1 (  +  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
)
3929, 38wa 360 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  +  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) )
4039, 27wex 1551 . . . . 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 2712 . . . 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 359 . . 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 5445 . 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 1653 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  12512  sumeq1f  12513  nfsum1  12515  nfsum  12516  sumeq2w  12517  sumeq2ii  12518  cbvsum  12520  zsum  12543  fsum  12545
  Copyright terms: Public domain W3C validator