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

Definition df-isum 10743
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. (Contributed by Jim Kingdon, 15-Feb-2022.)
Assertion
Ref Expression
df-isum  |-  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 ) ) ,  CC )  ~~>  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 ) ) ,  CC ) `
 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-isum
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 vk . . 3  setvar  k
41, 2, 3csu 10742 . 2  class  sum_ k  e.  A  B
5 vm . . . . . . . . 9  setvar  m
65cv 1288 . . . . . . . 8  class  m
7 cuz 9019 . . . . . . . 8  class  ZZ>=
86, 7cfv 5015 . . . . . . 7  class  ( ZZ>= `  m )
91, 8wss 2999 . . . . . 6  wff  A  C_  ( ZZ>= `  m )
10 vj . . . . . . . . . 10  setvar  j
1110cv 1288 . . . . . . . . 9  class  j
1211, 1wcel 1438 . . . . . . . 8  wff  j  e.  A
1312wdc 780 . . . . . . 7  wff DECID  j  e.  A
1413, 10, 8wral 2359 . . . . . 6  wff  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A
15 caddc 7353 . . . . . . . 8  class  +
16 cc 7348 . . . . . . . 8  class  CC
17 vn . . . . . . . . 9  setvar  n
18 cz 8750 . . . . . . . . 9  class  ZZ
1917cv 1288 . . . . . . . . . . 11  class  n
2019, 1wcel 1438 . . . . . . . . . 10  wff  n  e.  A
213, 19, 2csb 2933 . . . . . . . . . 10  class  [_ n  /  k ]_ B
22 cc0 7350 . . . . . . . . . 10  class  0
2320, 21, 22cif 3393 . . . . . . . . 9  class  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
2417, 18, 23cmpt 3899 . . . . . . . 8  class  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2515, 16, 24, 6cseq4 9851 . . . . . . 7  class  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )
26 vx . . . . . . . 8  setvar  x
2726cv 1288 . . . . . . 7  class  x
28 cli 10666 . . . . . . 7  class  ~~>
2925, 27, 28wbr 3845 . . . . . 6  wff  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x
309, 14, 29w3a 924 . . . . 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 ) ) ,  CC )  ~~>  x )
3130, 5, 18wrex 2360 . . . 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 ) ) ,  CC )  ~~>  x )
32 c1 7351 . . . . . . . . 9  class  1
33 cfz 9424 . . . . . . . . 9  class  ...
3432, 6, 33co 5652 . . . . . . . 8  class  ( 1 ... m )
35 vf . . . . . . . . 9  setvar  f
3635cv 1288 . . . . . . . 8  class  f
3734, 1, 36wf1o 5014 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> A
38 cn 8422 . . . . . . . . . . 11  class  NN
39 cle 7523 . . . . . . . . . . . . 13  class  <_
4019, 6, 39wbr 3845 . . . . . . . . . . . 12  wff  n  <_  m
4119, 36cfv 5015 . . . . . . . . . . . . 13  class  ( f `
 n )
423, 41, 2csb 2933 . . . . . . . . . . . 12  class  [_ (
f `  n )  /  k ]_ B
4340, 42, 22cif 3393 . . . . . . . . . . 11  class  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 )
4417, 38, 43cmpt 3899 . . . . . . . . . 10  class  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
4515, 16, 44, 32cseq4 9851 . . . . . . . . 9  class  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ,  CC )
466, 45cfv 5015 . . . . . . . 8  class  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ,  CC ) `
 m )
4727, 46wceq 1289 . . . . . . 7  wff  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ,  CC ) `
 m )
4837, 47wa 102 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ,  CC ) `
 m ) )
4948, 35wex 1426 . . . . 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 ) ) ,  CC ) `
 m ) )
5049, 5, 38wrex 2360 . . . 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 ) ) ,  CC ) `
 m ) )
5131, 50wo 664 . . 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 ) ) ,  CC )  ~~>  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 ) ) ,  CC ) `
 m ) ) )
5251, 26cio 4978 . 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 ) ) ,  CC )  ~~>  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 ) ) ,  CC ) `
 m ) ) ) )
534, 52wceq 1289 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 ) ) ,  CC )  ~~>  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 ) ) ,  CC ) `
 m ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  sumeq1  10744  nfsum1  10745  nfsum  10746  sumeq2  10748  cbvsum  10749  zisum  10774  fisum  10778
  Copyright terms: Public domain W3C validator