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

Definition df-sumdc 11361
Description: Define the sum of a series with an index set of integers 𝐴. The variable 𝑘 is normally a free variable in 𝐵, i.e., 𝐵 can be thought of as 𝐵(𝑘). 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 𝐵 to be defined where 𝑘𝐴. 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: Σ𝑘 ∈ {1, 2, 4}𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ(1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 11529). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)
Assertion
Ref Expression
df-sumdc Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚))))
Distinct variable groups:   𝑓,𝑘,𝑚,𝑛,𝑥,𝑗   𝐴,𝑓,𝑚,𝑛,𝑥,𝑗   𝐵,𝑓,𝑚,𝑛,𝑥,𝑗
Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Detailed syntax breakdown of Definition df-sumdc
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 vk . . 3 setvar 𝑘
41, 2, 3csu 11360 . 2 class Σ𝑘𝐴 𝐵
5 vm . . . . . . . . 9 setvar 𝑚
65cv 1352 . . . . . . . 8 class 𝑚
7 cuz 9527 . . . . . . . 8 class
86, 7cfv 5216 . . . . . . 7 class (ℤ𝑚)
91, 8wss 3129 . . . . . 6 wff 𝐴 ⊆ (ℤ𝑚)
10 vj . . . . . . . . . 10 setvar 𝑗
1110cv 1352 . . . . . . . . 9 class 𝑗
1211, 1wcel 2148 . . . . . . . 8 wff 𝑗𝐴
1312wdc 834 . . . . . . 7 wff DECID 𝑗𝐴
1413, 10, 8wral 2455 . . . . . 6 wff 𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴
15 caddc 7813 . . . . . . . 8 class +
16 vn . . . . . . . . 9 setvar 𝑛
17 cz 9252 . . . . . . . . 9 class
1816cv 1352 . . . . . . . . . . 11 class 𝑛
1918, 1wcel 2148 . . . . . . . . . 10 wff 𝑛𝐴
203, 18, 2csb 3057 . . . . . . . . . 10 class 𝑛 / 𝑘𝐵
21 cc0 7810 . . . . . . . . . 10 class 0
2219, 20, 21cif 3534 . . . . . . . . 9 class if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
2316, 17, 22cmpt 4064 . . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
2415, 23, 6cseq 10444 . . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)))
25 vx . . . . . . . 8 setvar 𝑥
2625cv 1352 . . . . . . 7 class 𝑥
27 cli 11285 . . . . . . 7 class
2824, 26, 27wbr 4003 . . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥
299, 14, 28w3a 978 . . . . 5 wff (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥)
3029, 5, 17wrex 2456 . . . 4 wff 𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥)
31 c1 7811 . . . . . . . . 9 class 1
32 cfz 10007 . . . . . . . . 9 class ...
3331, 6, 32co 5874 . . . . . . . 8 class (1...𝑚)
34 vf . . . . . . . . 9 setvar 𝑓
3534cv 1352 . . . . . . . 8 class 𝑓
3633, 1, 35wf1o 5215 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
37 cn 8918 . . . . . . . . . . 11 class
38 cle 7992 . . . . . . . . . . . . 13 class
3918, 6, 38wbr 4003 . . . . . . . . . . . 12 wff 𝑛𝑚
4018, 35cfv 5216 . . . . . . . . . . . . 13 class (𝑓𝑛)
413, 40, 2csb 3057 . . . . . . . . . . . 12 class (𝑓𝑛) / 𝑘𝐵
4239, 41, 21cif 3534 . . . . . . . . . . 11 class if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)
4316, 37, 42cmpt 4064 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0))
4415, 43, 31cseq 10444 . . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))
456, 44cfv 5216 . . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚)
4626, 45wceq 1353 . . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚)
4736, 46wa 104 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚))
4847, 34wex 1492 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚))
4948, 5, 37wrex 2456 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚))
5030, 49wo 708 . . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚)))
5150, 25cio 5176 . 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚))))
524, 51wceq 1353 1 wff Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚))))
Colors of variables: wff set class
This definition is referenced by:  sumeq1  11362  nfsum1  11363  nfsum  11364  sumeq2  11366  cbvsum  11367  zsumdc  11391  fsum3  11394
  Copyright terms: Public domain W3C validator