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 14882
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 sets of integers) by summo 14912. Examples: Σ𝑘 ∈ {1, 2, 4} 𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15076). (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 14881 . 2 class Σ𝑘𝐴 𝐵
5 vm . . . . . . . . 9 setvar 𝑚
65cv 1521 . . . . . . . 8 class 𝑚
7 cuz 12098 . . . . . . . 8 class
86, 7cfv 6230 . . . . . . 7 class (ℤ𝑚)
91, 8wss 3863 . . . . . 6 wff 𝐴 ⊆ (ℤ𝑚)
10 caddc 10391 . . . . . . . 8 class +
11 vn . . . . . . . . 9 setvar 𝑛
12 cz 11834 . . . . . . . . 9 class
1311cv 1521 . . . . . . . . . . 11 class 𝑛
1413, 1wcel 2081 . . . . . . . . . 10 wff 𝑛𝐴
153, 13, 2csb 3815 . . . . . . . . . 10 class 𝑛 / 𝑘𝐵
16 cc0 10388 . . . . . . . . . 10 class 0
1714, 15, 16cif 4385 . . . . . . . . 9 class if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
1811, 12, 17cmpt 5045 . . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
1910, 18, 6cseq 13224 . . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)))
20 vx . . . . . . . 8 setvar 𝑥
2120cv 1521 . . . . . . 7 class 𝑥
22 cli 14680 . . . . . . 7 class
2319, 21, 22wbr 4966 . . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥
249, 23wa 396 . . . . 5 wff (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥)
2524, 5, 12wrex 3106 . . . 4 wff 𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥)
26 c1 10389 . . . . . . . . 9 class 1
27 cfz 12747 . . . . . . . . 9 class ...
2826, 6, 27co 7021 . . . . . . . 8 class (1...𝑚)
29 vf . . . . . . . . 9 setvar 𝑓
3029cv 1521 . . . . . . . 8 class 𝑓
3128, 1, 30wf1o 6229 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
32 cn 11491 . . . . . . . . . . 11 class
3313, 30cfv 6230 . . . . . . . . . . . 12 class (𝑓𝑛)
343, 33, 2csb 3815 . . . . . . . . . . 11 class (𝑓𝑛) / 𝑘𝐵
3511, 32, 34cmpt 5045 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
3610, 35, 26cseq 13224 . . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
376, 36cfv 6230 . . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3821, 37wceq 1522 . . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3931, 38wa 396 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4039, 29wex 1761 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4140, 5, 32wrex 3106 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4225, 41wo 842 . . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
4342, 20cio 6192 . 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
444, 43wceq 1522 1 wff Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
Colors of variables: wff setvar class
This definition is referenced by:  sumex  14883  sumeq1  14884  nfsum1  14885  nfsum  14886  sumeq2w  14887  sumeq2ii  14888  cbvsum  14890  zsum  14913  fsum  14915
  Copyright terms: Public domain W3C validator