Definition df-sum 15596

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. These two methods of summation produce the same result on their common region of definition (i.e., finite sets of integers) by summo 15626. Examples: Σ𝑘 ∈ {1, 2, 4}𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ(1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15791). (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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		vk	. . 3 setvar 𝑘
4	1, 2, 3	csu 15595	. 2 class Σ𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . 9 setvar 𝑚
6	5	cv 1540	. . . . . . . 8 class 𝑚
7		cuz 12738	. . . . . . . 8 class ℤ≥
8	6, 7	cfv 6486	. . . . . . 7 class (ℤ≥‘𝑚)
9	1, 8	wss 3898	. . . . . 6 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		caddc 11016	. . . . . . . 8 class +
11		vn	. . . . . . . . 9 setvar 𝑛
12		cz 12475	. . . . . . . . 9 class ℤ
13	11	cv 1540	. . . . . . . . . . 11 class 𝑛
14	13, 1	wcel 2113	. . . . . . . . . 10 wff 𝑛 ∈ 𝐴
15	3, 13, 2	csb 3846	. . . . . . . . . 10 class ⦋𝑛 / 𝑘⦌𝐵
16		cc0 11013	. . . . . . . . . 10 class 0
17	14, 15, 16	cif 4474	. . . . . . . . 9 class if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
18	11, 12, 17	cmpt 5174	. . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
19	10, 18, 6	cseq 13910	. . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)))
20		vx	. . . . . . . 8 setvar 𝑥
21	20	cv 1540	. . . . . . 7 class 𝑥
22		cli 15393	. . . . . . 7 class ⇝
23	19, 21, 22	wbr 5093	. . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥
24	9, 23	wa 395	. . . . 5 wff (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
25	24, 5, 12	wrex 3057	. . . 4 wff ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
26		c1 11014	. . . . . . . . 9 class 1
27		cfz 13409	. . . . . . . . 9 class ...
28	26, 6, 27	co 7352	. . . . . . . 8 class (1...𝑚)
29		vf	. . . . . . . . 9 setvar 𝑓
30	29	cv 1540	. . . . . . . 8 class 𝑓
31	28, 1, 30	wf1o 6485	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
32		cn 12132	. . . . . . . . . . 11 class ℕ
33	13, 30	cfv 6486	. . . . . . . . . . . 12 class (𝑓‘𝑛)
34	3, 33, 2	csb 3846	. . . . . . . . . . 11 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
35	11, 32, 34	cmpt 5174	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
36	10, 35, 26	cseq 13910	. . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))
37	6, 36	cfv 6486	. . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
38	21, 37	wceq 1541	. . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
39	31, 38	wa 395	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
40	39, 29	wex 1780	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
41	40, 5, 32	wrex 3057	. . . 4 wff ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
42	25, 41	wo 847	. . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
43	42, 20	cio 6440	. 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
44	4, 43	wceq 1541	1 wff Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))

This definition is referenced by:  sumex  15597  sumeq1  15598  nfsum1  15599  nfsum  15600  sumeq2w  15601  sumeq2ii  15602  cbvsum  15604  cbvsumv  15605  sumeq2sdv  15612  zsum  15627  fsum  15629  sumeq2si  36267  cbvsumdavw  36344  cbvsumdavw2  36360