ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-sum Unicode version

Definition df-sum 9873
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). 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. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Assertion
Ref Expression
df-sum  |-  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x )  \/  E. m  e.  NN  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ,  CC ) `  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  setvar  k
41, 2, 3csu 9872 . 2  class  sum_ k  e.  A  B
5 vm . . . . . . . . 9  setvar  m
65cv 1242 . . . . . . . 8  class  m
7 cuz 8473 . . . . . . . 8  class  ZZ>=
86, 7cfv 4902 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 2917 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 caddc 6892 . . . . . . . 8  class  +
11 cc 6887 . . . . . . . 8  class  CC
12 vn . . . . . . . . 9  setvar  n
13 cz 8245 . . . . . . . . 9  class  ZZ
1412cv 1242 . . . . . . . . . . 11  class  n
1514, 1wcel 1393 . . . . . . . . . 10  wff  n  e.  A
163, 14, 2csb 2852 . . . . . . . . . 10  class  [_ n  /  k ]_ B
17 cc0 6889 . . . . . . . . . 10  class  0
1815, 16, 17cif 3331 . . . . . . . . 9  class  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
1912, 13, 18cmpt 3818 . . . . . . . 8  class  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2010, 11, 19, 6cseq 9211 . . . . . . 7  class  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )
21 vx . . . . . . . 8  setvar  x
2221cv 1242 . . . . . . 7  class  x
23 cli 9799 . . . . . . 7  class  ~~>
2420, 22, 23wbr 3764 . . . . . 6  wff  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x
259, 24wa 97 . . . . 5  wff  ( A 
C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x )
2625, 5, 13wrex 2307 . . . 4  wff  E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x )
27 c1 6890 . . . . . . . . 9  class  1
28 cfz 8874 . . . . . . . . 9  class  ...
2927, 6, 28co 5512 . . . . . . . 8  class  ( 1 ... m )
30 vf . . . . . . . . 9  setvar  f
3130cv 1242 . . . . . . . 8  class  f
3229, 1, 31wf1o 4901 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
33 cn 7914 . . . . . . . . . . 11  class  NN
3414, 31cfv 4902 . . . . . . . . . . . 12  class  ( f `
 n )
353, 34, 2csb 2852 . . . . . . . . . . 11  class  [_ (
f `  n )  /  k ]_ B
3612, 33, 35cmpt 3818 . . . . . . . . . 10  class  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
)
3710, 11, 36, 27cseq 9211 . . . . . . . . 9  class  seq 1
(  +  ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ,  CC )
386, 37cfv 4902 . . . . . . . 8  class  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ,  CC ) `  m )
3922, 38wceq 1243 . . . . . . 7  wff  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ,  CC ) `
 m )
4032, 39wa 97 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ,  CC ) `
 m ) )
4140, 30wex 1381 . . . . 5  wff  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ,  CC ) `  m )
)
4241, 5, 33wrex 2307 . . . 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 ) ,  CC ) `  m )
)
4326, 42wo 629 . . 3  wff  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x )  \/  E. m  e.  NN  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ,  CC ) `  m )
) )
4443, 21cio 4865 . 2  class  ( iota
x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ,  CC ) `  m )
) ) )
454, 44wceq 1243 1  wff  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x )  \/  E. m  e.  NN  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ,  CC ) `  m )
) ) )
Colors of variables: wff set class
This definition is referenced by:  sumeq1  9874  nfsum1  9875  nfsum  9876
  Copyright terms: Public domain W3C validator