ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-isum GIF version

Definition df-isum 10564
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. 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. (Contributed by Jim Kingdon, 15-Feb-2022.)
Assertion
Ref Expression
df-isum Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))))
Distinct variable groups:   𝑓,𝑘,𝑚,𝑛,𝑥,𝑗   𝐴,𝑓,𝑚,𝑛,𝑥,𝑗   𝐵,𝑓,𝑚,𝑛,𝑥,𝑗
Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Detailed syntax breakdown of Definition df-isum
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 vk . . 3 setvar 𝑘
41, 2, 3csu 10563 . 2 class Σ𝑘𝐴 𝐵
5 vm . . . . . . . . 9 setvar 𝑚
65cv 1284 . . . . . . . 8 class 𝑚
7 cuz 8913 . . . . . . . 8 class
86, 7cfv 4968 . . . . . . 7 class (ℤ𝑚)
91, 8wss 2984 . . . . . 6 wff 𝐴 ⊆ (ℤ𝑚)
10 vj . . . . . . . . . 10 setvar 𝑗
1110cv 1284 . . . . . . . . 9 class 𝑗
1211, 1wcel 1434 . . . . . . . 8 wff 𝑗𝐴
1312wdc 776 . . . . . . 7 wff DECID 𝑗𝐴
1413, 10, 8wral 2353 . . . . . 6 wff 𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴
15 caddc 7255 . . . . . . . 8 class +
16 cc 7250 . . . . . . . 8 class
17 vn . . . . . . . . 9 setvar 𝑛
18 cz 8645 . . . . . . . . 9 class
1917cv 1284 . . . . . . . . . . 11 class 𝑛
2019, 1wcel 1434 . . . . . . . . . 10 wff 𝑛𝐴
213, 19, 2csb 2919 . . . . . . . . . 10 class 𝑛 / 𝑘𝐵
22 cc0 7252 . . . . . . . . . 10 class 0
2320, 21, 22cif 3373 . . . . . . . . 9 class if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
2417, 18, 23cmpt 3865 . . . . . . . 8 class (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
2515, 16, 24, 6cseq 9739 . . . . . . 7 class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ)
26 vx . . . . . . . 8 setvar 𝑥
2726cv 1284 . . . . . . 7 class 𝑥
28 cli 10490 . . . . . . 7 class
2925, 27, 28wbr 3811 . . . . . 6 wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥
309, 14, 29w3a 920 . . . . 5 wff (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥)
3130, 5, 18wrex 2354 . . . 4 wff 𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥)
32 c1 7253 . . . . . . . . 9 class 1
33 cfz 9318 . . . . . . . . 9 class ...
3432, 6, 33co 5590 . . . . . . . 8 class (1...𝑚)
35 vf . . . . . . . . 9 setvar 𝑓
3635cv 1284 . . . . . . . 8 class 𝑓
3734, 1, 36wf1o 4967 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
38 cn 8315 . . . . . . . . . . 11 class
39 cle 7425 . . . . . . . . . . . . 13 class
4019, 6, 39wbr 3811 . . . . . . . . . . . 12 wff 𝑛𝑚
4119, 36cfv 4968 . . . . . . . . . . . . 13 class (𝑓𝑛)
423, 41, 2csb 2919 . . . . . . . . . . . 12 class (𝑓𝑛) / 𝑘𝐵
4340, 42, 22cif 3373 . . . . . . . . . . 11 class if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)
4417, 38, 43cmpt 3865 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0))
4515, 16, 44, 32cseq 9739 . . . . . . . . 9 class seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)
466, 45cfv 4968 . . . . . . . 8 class (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚)
4727, 46wceq 1285 . . . . . . 7 wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚)
4837, 47wa 102 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))
4948, 35wex 1422 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))
5049, 5, 38wrex 2354 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))
5131, 50wo 662 . . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚)))
5251, 26cio 4931 . 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))))
534, 52wceq 1285 1 wff Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))))
Colors of variables: wff set class
This definition is referenced by:  sumeq1  10565  nfsum1  10566  nfsum  10567  sumeq2d  10569  sumeq2  10570
  Copyright terms: Public domain W3C validator