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 14647
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 14678. Examples: Σ𝑘 ∈ {1, 2, 4} 𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 14842). (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 14646 . 2 class Σ𝑘𝐴 𝐵
5 vm . . . . . . . . 9 setvar 𝑚
65cv 1636 . . . . . . . 8 class 𝑚
7 cuz 11911 . . . . . . . 8 class
86, 7cfv 6108 . . . . . . 7 class (ℤ𝑚)
91, 8wss 3780 . . . . . 6 wff 𝐴 ⊆ (ℤ𝑚)
10 caddc 10231 . . . . . . . 8 class +
11 vn . . . . . . . . 9 setvar 𝑛
12 cz 11650 . . . . . . . . 9 class
1311cv 1636 . . . . . . . . . . 11 class 𝑛
1413, 1wcel 2157 . . . . . . . . . 10 wff 𝑛𝐴
153, 13, 2csb 3739 . . . . . . . . . 10 class 𝑛 / 𝑘𝐵
16 cc0 10228 . . . . . . . . . 10 class 0
1714, 15, 16cif 4290 . . . . . . . . 9 class if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
1811, 12, 17cmpt 4934 . . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
1910, 18, 6cseq 13031 . . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)))
20 vx . . . . . . . 8 setvar 𝑥
2120cv 1636 . . . . . . 7 class 𝑥
22 cli 14445 . . . . . . 7 class
2319, 21, 22wbr 4855 . . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥
249, 23wa 384 . . . . 5 wff (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥)
2524, 5, 12wrex 3108 . . . 4 wff 𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥)
26 c1 10229 . . . . . . . . 9 class 1
27 cfz 12556 . . . . . . . . 9 class ...
2826, 6, 27co 6881 . . . . . . . 8 class (1...𝑚)
29 vf . . . . . . . . 9 setvar 𝑓
3029cv 1636 . . . . . . . 8 class 𝑓
3128, 1, 30wf1o 6107 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
32 cn 11312 . . . . . . . . . . 11 class
3313, 30cfv 6108 . . . . . . . . . . . 12 class (𝑓𝑛)
343, 33, 2csb 3739 . . . . . . . . . . 11 class (𝑓𝑛) / 𝑘𝐵
3511, 32, 34cmpt 4934 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
3610, 35, 26cseq 13031 . . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
376, 36cfv 6108 . . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3821, 37wceq 1637 . . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3931, 38wa 384 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4039, 29wex 1859 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4140, 5, 32wrex 3108 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4225, 41wo 865 . . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
4342, 20cio 6069 . 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
444, 43wceq 1637 1 wff Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
Colors of variables: wff setvar class
This definition is referenced by:  sumex  14648  sumeq1  14649  nfsum1  14650  nfsum  14651  sumeq2w  14652  sumeq2ii  14653  cbvsum  14655  zsum  14679  fsum  14681
  Copyright terms: Public domain W3C validator