Definition df-sumdc 11916

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 12085). (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 11915	. 2 class Σ𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . 9 setvar 𝑚
6	5	cv 1396	. . . . . . . 8 class 𝑚
7		cuz 9755	. . . . . . . 8 class ℤ≥
8	6, 7	cfv 5326	. . . . . . 7 class (ℤ≥‘𝑚)
9	1, 8	wss 3200	. . . . . 6 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		vj	. . . . . . . . . 10 setvar 𝑗
11	10	cv 1396	. . . . . . . . 9 class 𝑗
12	11, 1	wcel 2202	. . . . . . . 8 wff 𝑗 ∈ 𝐴
13	12	wdc 841	. . . . . . 7 wff DECID 𝑗 ∈ 𝐴
14	13, 10, 8	wral 2510	. . . . . 6 wff ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴
15		caddc 8035	. . . . . . . 8 class +
16		vn	. . . . . . . . 9 setvar 𝑛
17		cz 9479	. . . . . . . . 9 class ℤ
18	16	cv 1396	. . . . . . . . . . 11 class 𝑛
19	18, 1	wcel 2202	. . . . . . . . . 10 wff 𝑛 ∈ 𝐴
20	3, 18, 2	csb 3127	. . . . . . . . . 10 class ⦋𝑛 / 𝑘⦌𝐵
21		cc0 8032	. . . . . . . . . 10 class 0
22	19, 20, 21	cif 3605	. . . . . . . . 9 class if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
23	16, 17, 22	cmpt 4150	. . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
24	15, 23, 6	cseq 10710	. . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)))
25		vx	. . . . . . . 8 setvar 𝑥
26	25	cv 1396	. . . . . . 7 class 𝑥
27		cli 11840	. . . . . . 7 class ⇝
28	24, 26, 27	wbr 4088	. . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥
29	9, 14, 28	w3a 1004	. . . . 5 wff (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
30	29, 5, 17	wrex 2511	. . . 4 wff ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
31		c1 8033	. . . . . . . . 9 class 1
32		cfz 10243	. . . . . . . . 9 class ...
33	31, 6, 32	co 6018	. . . . . . . 8 class (1...𝑚)
34		vf	. . . . . . . . 9 setvar 𝑓
35	34	cv 1396	. . . . . . . 8 class 𝑓
36	33, 1, 35	wf1o 5325	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
37		cn 9143	. . . . . . . . . . 11 class ℕ
38		cle 8215	. . . . . . . . . . . . 13 class ≤
39	18, 6, 38	wbr 4088	. . . . . . . . . . . 12 wff 𝑛 ≤ 𝑚
40	18, 35	cfv 5326	. . . . . . . . . . . . 13 class (𝑓‘𝑛)
41	3, 40, 2	csb 3127	. . . . . . . . . . . 12 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
42	39, 41, 21	cif 3605	. . . . . . . . . . 11 class if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)
43	16, 37, 42	cmpt 4150	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
44	15, 43, 31	cseq 10710	. . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
45	6, 44	cfv 5326	. . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)
46	26, 45	wceq 1397	. . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)
47	36, 46	wa 104	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
48	47, 34	wex 1540	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
49	48, 5, 37	wrex 2511	. . . 4 wff ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
50	30, 49	wo 715	. . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
51	50, 25	cio 5284	. 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
52	4, 51	wceq 1397	1 wff Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))

This definition is referenced by:  sumeq1  11917  nfsum1  11918  nfsum  11919  sumeq2  11921  cbvsum  11922  zsumdc  11947  fsum3  11950