Definition df-sum 15716

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 15746. Examples: Σ𝑘 ∈ {1, 2, 4}𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ(1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15914). (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 15715	. 2 class Σ𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . 9 setvar 𝑚
6	5	cv 1561	. . . . . . . 8 class 𝑚
7		cuz 12841	. . . . . . . 8 class ℤ≥
8	6, 7	cfv 6523	. . . . . . 7 class (ℤ≥‘𝑚)
9	1, 8	wss 3906	. . . . . 6 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		caddc 11078	. . . . . . . 8 class +
11		vn	. . . . . . . . 9 setvar 𝑛
12		cz 12570	. . . . . . . . 9 class ℤ
13	11	cv 1561	. . . . . . . . . . 11 class 𝑛
14	13, 1	wcel 2144	. . . . . . . . . 10 wff 𝑛 ∈ 𝐴
15	3, 13, 2	csb 3854	. . . . . . . . . 10 class ⦋𝑛 / 𝑘⦌𝐵
16		cc0 11075	. . . . . . . . . 10 class 0
17	14, 15, 16	cif 4482	. . . . . . . . 9 class if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
18	11, 12, 17	cmpt 5183	. . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
19	10, 18, 6	cseq 14016	. . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)))
20		vx	. . . . . . . 8 setvar 𝑥
21	20	cv 1561	. . . . . . 7 class 𝑥
22		cli 15513	. . . . . . 7 class ⇝
23	19, 21, 22	wbr 5102	. . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥
24	9, 23	wa 399	. . . . 5 wff (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
25	24, 5, 12	wrex 3088	. . . 4 wff ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
26		c1 11076	. . . . . . . . 9 class 1
27		cfz 13514	. . . . . . . . 9 class ...
28	26, 6, 27	co 7398	. . . . . . . 8 class (1...𝑚)
29		vf	. . . . . . . . 9 setvar 𝑓
30	29	cv 1561	. . . . . . . 8 class 𝑓
31	28, 1, 30	wf1o 6522	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
32		cn 12212	. . . . . . . . . . 11 class ℕ
33	13, 30	cfv 6523	. . . . . . . . . . . 12 class (𝑓‘𝑛)
34	3, 33, 2	csb 3854	. . . . . . . . . . 11 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
35	11, 32, 34	cmpt 5183	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
36	10, 35, 26	cseq 14016	. . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))
37	6, 36	cfv 6523	. . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
38	21, 37	wceq 1562	. . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
39	31, 38	wa 399	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
40	39, 29	wex 1801	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
41	40, 5, 32	wrex 3088	. . . 4 wff ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
42	25, 41	wo 858	. . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
43	42, 20	cio 6477	. 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
44	4, 43	wceq 1562	1 wff Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))

This definition is referenced by:  sumex  15717  sumeq1  15718  nfsum1  15719  nfsum  15720  sumeq2w  15721  sumeq2ii  15722  cbvsum  15724  cbvsumv  15725  sumeq2sdv  15732  zsum  15747  fsum  15749  sumeq2si  36567  cbvsumdavw  36644  cbvsumdavw2  36660