MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sum Structured version   Visualization version   GIF version

Definition df-sum 14213
Description: Define the sum of a series with an index set of integers 𝐴. 𝑘 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. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers) by summo 14243. Examples: Σ𝑘 ∈ {1, 2, 4} 𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 14401). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Assertion
Ref Expression
df-sum Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
Distinct variable groups:   𝑓,𝑘,𝑚,𝑛,𝑥   𝐴,𝑓,𝑚,𝑛,𝑥   𝐵,𝑓,𝑚,𝑛,𝑥
Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Detailed syntax breakdown of Definition df-sum
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 vk . . 3 setvar 𝑘
41, 2, 3csu 14212 . 2 class Σ𝑘𝐴 𝐵
5 vm . . . . . . . . 9 setvar 𝑚
65cv 1473 . . . . . . . 8 class 𝑚
7 cuz 11521 . . . . . . . 8 class
86, 7cfv 5789 . . . . . . 7 class (ℤ𝑚)
91, 8wss 3539 . . . . . 6 wff 𝐴 ⊆ (ℤ𝑚)
10 caddc 9795 . . . . . . . 8 class +
11 vn . . . . . . . . 9 setvar 𝑛
12 cz 11212 . . . . . . . . 9 class
1311cv 1473 . . . . . . . . . . 11 class 𝑛
1413, 1wcel 1976 . . . . . . . . . 10 wff 𝑛𝐴
153, 13, 2csb 3498 . . . . . . . . . 10 class 𝑛 / 𝑘𝐵
16 cc0 9792 . . . . . . . . . 10 class 0
1714, 15, 16cif 4035 . . . . . . . . 9 class if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
1811, 12, 17cmpt 4637 . . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
1910, 18, 6cseq 12620 . . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)))
20 vx . . . . . . . 8 setvar 𝑥
2120cv 1473 . . . . . . 7 class 𝑥
22 cli 14011 . . . . . . 7 class
2319, 21, 22wbr 4577 . . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥
249, 23wa 382 . . . . 5 wff (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥)
2524, 5, 12wrex 2896 . . . 4 wff 𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥)
26 c1 9793 . . . . . . . . 9 class 1
27 cfz 12154 . . . . . . . . 9 class ...
2826, 6, 27co 6526 . . . . . . . 8 class (1...𝑚)
29 vf . . . . . . . . 9 setvar 𝑓
3029cv 1473 . . . . . . . 8 class 𝑓
3128, 1, 30wf1o 5788 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
32 cn 10869 . . . . . . . . . . 11 class
3313, 30cfv 5789 . . . . . . . . . . . 12 class (𝑓𝑛)
343, 33, 2csb 3498 . . . . . . . . . . 11 class (𝑓𝑛) / 𝑘𝐵
3511, 32, 34cmpt 4637 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
3610, 35, 26cseq 12620 . . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
376, 36cfv 5789 . . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3821, 37wceq 1474 . . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3931, 38wa 382 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4039, 29wex 1694 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4140, 5, 32wrex 2896 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4225, 41wo 381 . . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
4342, 20cio 5751 . 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
444, 43wceq 1474 1 wff Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
Colors of variables: wff setvar class
This definition is referenced by:  sumex  14214  sumeq1  14215  nfsum1  14216  nfsum  14217  sumeq2w  14218  sumeq2ii  14219  cbvsum  14221  zsum  14244  fsum  14246
  Copyright terms: Public domain W3C validator