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 10190 |
. 2
class
Σ𝑘 ∈
𝐴 𝐵 |
5 | | vm |
. . . . . . . . 9
setvar 𝑚 |
6 | 5 | cv 1283 |
. . . . . . . 8
class 𝑚 |
7 | | cuz 8619 |
. . . . . . . 8
class
ℤ≥ |
8 | 6, 7 | cfv 4922 |
. . . . . . 7
class
(ℤ≥‘𝑚) |
9 | 1, 8 | wss 2973 |
. . . . . 6
wff 𝐴 ⊆
(ℤ≥‘𝑚) |
10 | | caddc 6984 |
. . . . . . . 8
class
+ |
11 | | cc 6979 |
. . . . . . . 8
class
ℂ |
12 | | vn |
. . . . . . . . 9
setvar 𝑛 |
13 | | cz 8351 |
. . . . . . . . 9
class
ℤ |
14 | 12 | cv 1283 |
. . . . . . . . . . 11
class 𝑛 |
15 | 14, 1 | wcel 1433 |
. . . . . . . . . 10
wff 𝑛 ∈ 𝐴 |
16 | 3, 14, 2 | csb 2908 |
. . . . . . . . . 10
class
⦋𝑛 /
𝑘⦌𝐵 |
17 | | cc0 6981 |
. . . . . . . . . 10
class
0 |
18 | 15, 16, 17 | cif 3351 |
. . . . . . . . 9
class if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) |
19 | 12, 13, 18 | cmpt 3839 |
. . . . . . . 8
class (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
20 | 10, 11, 19, 6 | cseq 9431 |
. . . . . . 7
class seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) |
21 | | vx |
. . . . . . . 8
setvar 𝑥 |
22 | 21 | cv 1283 |
. . . . . . 7
class 𝑥 |
23 | | cli 10117 |
. . . . . . 7
class
⇝ |
24 | 20, 22, 23 | wbr 3785 |
. . . . . 6
wff seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑥 |
25 | 9, 24 | wa 102 |
. . . . 5
wff (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑥) |
26 | 25, 5, 13 | wrex 2349 |
. . . 4
wff
∃𝑚 ∈
ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑥) |
27 | | c1 6982 |
. . . . . . . . 9
class
1 |
28 | | cfz 9029 |
. . . . . . . . 9
class
... |
29 | 27, 6, 28 | co 5532 |
. . . . . . . 8
class
(1...𝑚) |
30 | | vf |
. . . . . . . . 9
setvar 𝑓 |
31 | 30 | cv 1283 |
. . . . . . . 8
class 𝑓 |
32 | 29, 1, 31 | wf1o 4921 |
. . . . . . 7
wff 𝑓:(1...𝑚)–1-1-onto→𝐴 |
33 | | cn 8039 |
. . . . . . . . . . 11
class
ℕ |
34 | 14, 31 | cfv 4922 |
. . . . . . . . . . . 12
class (𝑓‘𝑛) |
35 | 3, 34, 2 | csb 2908 |
. . . . . . . . . . 11
class
⦋(𝑓‘𝑛) / 𝑘⦌𝐵 |
36 | 12, 33, 35 | cmpt 3839 |
. . . . . . . . . 10
class (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
37 | 10, 11, 36, 27 | cseq 9431 |
. . . . . . . . 9
class seq1( + ,
(𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ) |
38 | 6, 37 | cfv 4922 |
. . . . . . . 8
class (seq1( +
, (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚) |
39 | 22, 38 | wceq 1284 |
. . . . . . 7
wff 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚) |
40 | 32, 39 | wa 102 |
. . . . . 6
wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)) |
41 | 40, 30 | wex 1421 |
. . . . 5
wff
∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)) |
42 | 41, 5, 33 | wrex 2349 |
. . . 4
wff
∃𝑚 ∈
ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)) |
43 | 26, 42 | wo 661 |
. . 3
wff
(∃𝑚 ∈
ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚))) |
44 | 43, 21 | cio 4885 |
. 2
class
(℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)))) |
45 | 4, 44 | wceq 1284 |
1
wff
Σ𝑘 ∈
𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)))) |