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

Definition df-sumdc 11154
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 11322). (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 11153 . 2  class  sum_ k  e.  A  B
5 vm . . . . . . . . 9  setvar  m
65cv 1331 . . . . . . . 8  class  m
7 cuz 9349 . . . . . . . 8  class  ZZ>=
86, 7cfv 5130 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 3075 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 vj . . . . . . . . . 10  setvar  j
1110cv 1331 . . . . . . . . 9  class  j
1211, 1wcel 1481 . . . . . . . 8  wff  j  e.  A
1312wdc 820 . . . . . . 7  wff DECID  j  e.  A
1413, 10, 8wral 2417 . . . . . 6  wff  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A
15 caddc 7646 . . . . . . . 8  class  +
16 vn . . . . . . . . 9  setvar  n
17 cz 9077 . . . . . . . . 9  class  ZZ
1816cv 1331 . . . . . . . . . . 11  class  n
1918, 1wcel 1481 . . . . . . . . . 10  wff  n  e.  A
203, 18, 2csb 3006 . . . . . . . . . 10  class  [_ n  /  k ]_ B
21 cc0 7643 . . . . . . . . . 10  class  0
2219, 20, 21cif 3478 . . . . . . . . 9  class  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
2316, 17, 22cmpt 3996 . . . . . . . 8  class  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2415, 23, 6cseq 10248 . . . . . . 7  class  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )
25 vx . . . . . . . 8  setvar  x
2625cv 1331 . . . . . . 7  class  x
27 cli 11078 . . . . . . 7  class  ~~>
2824, 26, 27wbr 3936 . . . . . 6  wff  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x
299, 14, 28w3a 963 . . . . 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 2418 . . . 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 7644 . . . . . . . . 9  class  1
32 cfz 9820 . . . . . . . . 9  class  ...
3331, 6, 32co 5781 . . . . . . . 8  class  ( 1 ... m )
34 vf . . . . . . . . 9  setvar  f
3534cv 1331 . . . . . . . 8  class  f
3633, 1, 35wf1o 5129 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
37 cn 8743 . . . . . . . . . . 11  class  NN
38 cle 7824 . . . . . . . . . . . . 13  class  <_
3918, 6, 38wbr 3936 . . . . . . . . . . . 12  wff  n  <_  m
4018, 35cfv 5130 . . . . . . . . . . . . 13  class  ( f `
 n )
413, 40, 2csb 3006 . . . . . . . . . . . 12  class  [_ (
f `  n )  /  k ]_ B
4239, 41, 21cif 3478 . . . . . . . . . . 11  class  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 )
4316, 37, 42cmpt 3996 . . . . . . . . . 10  class  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
4415, 43, 31cseq 10248 . . . . . . . . 9  class  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) )
456, 44cfv 5130 . . . . . . . 8  class  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
)
4626, 45wceq 1332 . . . . . . 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 1469 . . . . 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 2418 . . . 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 698 . . 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 5093 . 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 1332 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  11155  nfsum1  11156  nfsum  11157  sumeq2  11159  cbvsum  11160  zsumdc  11184  fsum3  11187
  Copyright terms: Public domain W3C validator