Definition df-sumdc 11346

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. In both cases we have an if expression so that we only need 𝐵 to be defined where 𝑘 ∈ 𝐴. In the infinite case, we also require that the indexing set be a decidable subset of an upperset of integers (that is, membership of integers in it is decidable). These two methods of summation produce the same result on their common region of definition (i.e., finite sets of integers). Examples: Σ𝑘 ∈ {1, 2, 4}𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ(1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 11514). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)

Assertion

Ref	Expression
df-sumdc	⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))

Distinct variable groups:   𝑓,𝑘,𝑚,𝑛,𝑥,𝑗   𝐴,𝑓,𝑚,𝑛,𝑥,𝑗   𝐵,𝑓,𝑚,𝑛,𝑥,𝑗

Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Detailed syntax breakdown of Definition df-sumdc

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		vk	. . 3 setvar 𝑘
4	1, 2, 3	csu 11345	. 2 class Σ𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . 9 setvar 𝑚
6	5	cv 1352	. . . . . . . 8 class 𝑚
7		cuz 9517	. . . . . . . 8 class ℤ≥
8	6, 7	cfv 5212	. . . . . . 7 class (ℤ≥‘𝑚)
9	1, 8	wss 3129	. . . . . 6 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		vj	. . . . . . . . . 10 setvar 𝑗
11	10	cv 1352	. . . . . . . . 9 class 𝑗
12	11, 1	wcel 2148	. . . . . . . 8 wff 𝑗 ∈ 𝐴
13	12	wdc 834	. . . . . . 7 wff DECID 𝑗 ∈ 𝐴
14	13, 10, 8	wral 2455	. . . . . 6 wff ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴
15		caddc 7805	. . . . . . . 8 class +
16		vn	. . . . . . . . 9 setvar 𝑛
17		cz 9242	. . . . . . . . 9 class ℤ
18	16	cv 1352	. . . . . . . . . . 11 class 𝑛
19	18, 1	wcel 2148	. . . . . . . . . 10 wff 𝑛 ∈ 𝐴
20	3, 18, 2	csb 3057	. . . . . . . . . 10 class ⦋𝑛 / 𝑘⦌𝐵
21		cc0 7802	. . . . . . . . . 10 class 0
22	19, 20, 21	cif 3534	. . . . . . . . 9 class if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
23	16, 17, 22	cmpt 4061	. . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
24	15, 23, 6	cseq 10431	. . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)))
25		vx	. . . . . . . 8 setvar 𝑥
26	25	cv 1352	. . . . . . 7 class 𝑥
27		cli 11270	. . . . . . 7 class ⇝
28	24, 26, 27	wbr 4000	. . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥
29	9, 14, 28	w3a 978	. . . . 5 wff (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
30	29, 5, 17	wrex 2456	. . . 4 wff ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
31		c1 7803	. . . . . . . . 9 class 1
32		cfz 9995	. . . . . . . . 9 class ...
33	31, 6, 32	co 5869	. . . . . . . 8 class (1...𝑚)
34		vf	. . . . . . . . 9 setvar 𝑓
35	34	cv 1352	. . . . . . . 8 class 𝑓
36	33, 1, 35	wf1o 5211	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
37		cn 8908	. . . . . . . . . . 11 class ℕ
38		cle 7983	. . . . . . . . . . . . 13 class ≤
39	18, 6, 38	wbr 4000	. . . . . . . . . . . 12 wff 𝑛 ≤ 𝑚
40	18, 35	cfv 5212	. . . . . . . . . . . . 13 class (𝑓‘𝑛)
41	3, 40, 2	csb 3057	. . . . . . . . . . . 12 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
42	39, 41, 21	cif 3534	. . . . . . . . . . 11 class if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)
43	16, 37, 42	cmpt 4061	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
44	15, 43, 31	cseq 10431	. . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
45	6, 44	cfv 5212	. . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)
46	26, 45	wceq 1353	. . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)
47	36, 46	wa 104	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
48	47, 34	wex 1492	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
49	48, 5, 37	wrex 2456	. . . 4 wff ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
50	30, 49	wo 708	. . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
51	50, 25	cio 5172	. 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
52	4, 51	wceq 1353	1 wff Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))

This definition is referenced by:  sumeq1  11347  nfsum1  11348  nfsum  11349  sumeq2  11351  cbvsum  11352  zsumdc  11376  fsum3  11379