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

Definition df-sumdc 10962
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. In both cases we have an  if expression so that we only need  B to be defined where  k  e.  A. In the infinite case, we also require that the indexing set be a decidable subset of an upperset of integers (that is, membership of integers in it is decidable). These two methods of summation produce the same result on their common region of definition (i.e. finite sets of 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 (geoihalfsum 11130). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)
Assertion
Ref Expression
df-sumdc  |-  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
Distinct variable groups:    f, k, m, n, x, j    A, f, m, n, x, j    B, f, m, n, x, j
Allowed substitution hints:    A( k)    B( k)

Detailed syntax breakdown of Definition df-sumdc
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 vk . . 3  setvar  k
41, 2, 3csu 10961 . 2  class  sum_ k  e.  A  B
5 vm . . . . . . . . 9  setvar  m
65cv 1298 . . . . . . . 8  class  m
7 cuz 9176 . . . . . . . 8  class  ZZ>=
86, 7cfv 5059 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 3021 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 vj . . . . . . . . . 10  setvar  j
1110cv 1298 . . . . . . . . 9  class  j
1211, 1wcel 1448 . . . . . . . 8  wff  j  e.  A
1312wdc 786 . . . . . . 7  wff DECID  j  e.  A
1413, 10, 8wral 2375 . . . . . 6  wff  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A
15 caddc 7503 . . . . . . . 8  class  +
16 vn . . . . . . . . 9  setvar  n
17 cz 8906 . . . . . . . . 9  class  ZZ
1816cv 1298 . . . . . . . . . . 11  class  n
1918, 1wcel 1448 . . . . . . . . . 10  wff  n  e.  A
203, 18, 2csb 2955 . . . . . . . . . 10  class  [_ n  /  k ]_ B
21 cc0 7500 . . . . . . . . . 10  class  0
2219, 20, 21cif 3421 . . . . . . . . 9  class  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
2316, 17, 22cmpt 3929 . . . . . . . 8  class  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2415, 23, 6cseq 10059 . . . . . . 7  class  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )
25 vx . . . . . . . 8  setvar  x
2625cv 1298 . . . . . . 7  class  x
27 cli 10886 . . . . . . 7  class  ~~>
2824, 26, 27wbr 3875 . . . . . 6  wff  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x
299, 14, 28w3a 930 . . . . 5  wff  ( A 
C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )
3029, 5, 17wrex 2376 . . . 4  wff  E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )
31 c1 7501 . . . . . . . . 9  class  1
32 cfz 9631 . . . . . . . . 9  class  ...
3331, 6, 32co 5706 . . . . . . . 8  class  ( 1 ... m )
34 vf . . . . . . . . 9  setvar  f
3534cv 1298 . . . . . . . 8  class  f
3633, 1, 35wf1o 5058 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
37 cn 8578 . . . . . . . . . . 11  class  NN
38 cle 7673 . . . . . . . . . . . . 13  class  <_
3918, 6, 38wbr 3875 . . . . . . . . . . . 12  wff  n  <_  m
4018, 35cfv 5059 . . . . . . . . . . . . 13  class  ( f `
 n )
413, 40, 2csb 2955 . . . . . . . . . . . 12  class  [_ (
f `  n )  /  k ]_ B
4239, 41, 21cif 3421 . . . . . . . . . . 11  class  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 )
4316, 37, 42cmpt 3929 . . . . . . . . . 10  class  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
4415, 43, 31cseq 10059 . . . . . . . . 9  class  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) )
456, 44cfv 5059 . . . . . . . 8  class  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
)
4626, 45wceq 1299 . . . . . . 7  wff  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
)
4736, 46wa 103 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) )
4847, 34wex 1436 . . . . 5  wff  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) )
4948, 5, 37wrex 2376 . . . 4  wff  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) )
5030, 49wo 670 . . 3  wff  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) )
5150, 25cio 5022 . 2  class  ( iota
x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
524, 51wceq 1299 1  wff  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
Colors of variables: wff set class
This definition is referenced by:  sumeq1  10963  nfsum1  10964  nfsum  10965  sumeq2  10967  cbvsum  10968  zsumdc  10992  fsum3  10995
  Copyright terms: Public domain W3C validator