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

Definition df-sumdc 11394
Description: Define the sum of a series with an index set of integers  A. The variable  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 11562). (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 11393 . 2  class  sum_ k  e.  A  B
5 vm . . . . . . . . 9  setvar  m
65cv 1363 . . . . . . . 8  class  m
7 cuz 9558 . . . . . . . 8  class  ZZ>=
86, 7cfv 5235 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 3144 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 vj . . . . . . . . . 10  setvar  j
1110cv 1363 . . . . . . . . 9  class  j
1211, 1wcel 2160 . . . . . . . 8  wff  j  e.  A
1312wdc 835 . . . . . . 7  wff DECID  j  e.  A
1413, 10, 8wral 2468 . . . . . 6  wff  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A
15 caddc 7844 . . . . . . . 8  class  +
16 vn . . . . . . . . 9  setvar  n
17 cz 9283 . . . . . . . . 9  class  ZZ
1816cv 1363 . . . . . . . . . . 11  class  n
1918, 1wcel 2160 . . . . . . . . . 10  wff  n  e.  A
203, 18, 2csb 3072 . . . . . . . . . 10  class  [_ n  /  k ]_ B
21 cc0 7841 . . . . . . . . . 10  class  0
2219, 20, 21cif 3549 . . . . . . . . 9  class  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
2316, 17, 22cmpt 4079 . . . . . . . 8  class  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2415, 23, 6cseq 10476 . . . . . . 7  class  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )
25 vx . . . . . . . 8  setvar  x
2625cv 1363 . . . . . . 7  class  x
27 cli 11318 . . . . . . 7  class  ~~>
2824, 26, 27wbr 4018 . . . . . 6  wff  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x
299, 14, 28w3a 980 . . . . 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 2469 . . . 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 7842 . . . . . . . . 9  class  1
32 cfz 10038 . . . . . . . . 9  class  ...
3331, 6, 32co 5896 . . . . . . . 8  class  ( 1 ... m )
34 vf . . . . . . . . 9  setvar  f
3534cv 1363 . . . . . . . 8  class  f
3633, 1, 35wf1o 5234 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
37 cn 8949 . . . . . . . . . . 11  class  NN
38 cle 8023 . . . . . . . . . . . . 13  class  <_
3918, 6, 38wbr 4018 . . . . . . . . . . . 12  wff  n  <_  m
4018, 35cfv 5235 . . . . . . . . . . . . 13  class  ( f `
 n )
413, 40, 2csb 3072 . . . . . . . . . . . 12  class  [_ (
f `  n )  /  k ]_ B
4239, 41, 21cif 3549 . . . . . . . . . . 11  class  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 )
4316, 37, 42cmpt 4079 . . . . . . . . . 10  class  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
4415, 43, 31cseq 10476 . . . . . . . . 9  class  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) )
456, 44cfv 5235 . . . . . . . 8  class  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
)
4626, 45wceq 1364 . . . . . . 7  wff  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
)
4736, 46wa 104 . . . . . 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 1503 . . . . 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 2469 . . . 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 709 . . 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 5194 . 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 1364 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  11395  nfsum1  11396  nfsum  11397  sumeq2  11399  cbvsum  11400  zsumdc  11424  fsum3  11427
  Copyright terms: Public domain W3C validator