Step | Hyp | Ref
| Expression |
1 | | df-sum 9873 |
. 2
⊢
Σ𝑘 ∈
𝐴 𝐵 = (℩𝑧(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)))) |
2 | | nfcv 2178 |
. . . . 5
⊢
Ⅎ𝑥ℤ |
3 | | nfsum.1 |
. . . . . . 7
⊢
Ⅎ𝑥𝐴 |
4 | | nfcv 2178 |
. . . . . . 7
⊢
Ⅎ𝑥(ℤ≥‘𝑚) |
5 | 3, 4 | nfss 2938 |
. . . . . 6
⊢
Ⅎ𝑥 𝐴 ⊆
(ℤ≥‘𝑚) |
6 | | nfcv 2178 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑚 |
7 | | nfcv 2178 |
. . . . . . . 8
⊢
Ⅎ𝑥
+ |
8 | 3 | nfcri 2172 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑛 ∈ 𝐴 |
9 | | nfcv 2178 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑛 |
10 | | nfsum.2 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐵 |
11 | 9, 10 | nfcsb 2884 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑛 / 𝑘⦌𝐵 |
12 | | nfcv 2178 |
. . . . . . . . . 10
⊢
Ⅎ𝑥0 |
13 | 8, 11, 12 | nfif 3356 |
. . . . . . . . 9
⊢
Ⅎ𝑥if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) |
14 | 2, 13 | nfmpt 3849 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
15 | | nfcv 2178 |
. . . . . . . 8
⊢
Ⅎ𝑥ℂ |
16 | 6, 7, 14, 15 | nfiseq 9218 |
. . . . . . 7
⊢
Ⅎ𝑥seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) |
17 | | nfcv 2178 |
. . . . . . 7
⊢
Ⅎ𝑥
⇝ |
18 | | nfcv 2178 |
. . . . . . 7
⊢
Ⅎ𝑥𝑧 |
19 | 16, 17, 18 | nfbr 3808 |
. . . . . 6
⊢
Ⅎ𝑥seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑧 |
20 | 5, 19 | nfan 1457 |
. . . . 5
⊢
Ⅎ𝑥(𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑧) |
21 | 2, 20 | nfrexya 2363 |
. . . 4
⊢
Ⅎ𝑥∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑧) |
22 | | nfcv 2178 |
. . . . 5
⊢
Ⅎ𝑥ℕ |
23 | | nfcv 2178 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑓 |
24 | | nfcv 2178 |
. . . . . . . 8
⊢
Ⅎ𝑥(1...𝑚) |
25 | 23, 24, 3 | nff1o 5124 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑓:(1...𝑚)–1-1-onto→𝐴 |
26 | | nfcv 2178 |
. . . . . . . . . 10
⊢
Ⅎ𝑥1 |
27 | | nfcv 2178 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑓‘𝑛) |
28 | 27, 10 | nfcsb 2884 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋(𝑓‘𝑛) / 𝑘⦌𝐵 |
29 | 22, 28 | nfmpt 3849 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
30 | 26, 7, 29, 15 | nfiseq 9218 |
. . . . . . . . 9
⊢
Ⅎ𝑥seq1(
+ , (𝑛 ∈ ℕ
↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ) |
31 | 30, 6 | nffv 5185 |
. . . . . . . 8
⊢
Ⅎ𝑥(seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚) |
32 | 31 | nfeq2 2189 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚) |
33 | 25, 32 | nfan 1457 |
. . . . . 6
⊢
Ⅎ𝑥(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)) |
34 | 33 | nfex 1528 |
. . . . 5
⊢
Ⅎ𝑥∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)) |
35 | 22, 34 | nfrexya 2363 |
. . . 4
⊢
Ⅎ𝑥∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)) |
36 | 21, 35 | nfor 1466 |
. . 3
⊢
Ⅎ𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚))) |
37 | 36 | nfiotaxy 4871 |
. 2
⊢
Ⅎ𝑥(℩𝑧(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵), ℂ)‘𝑚)))) |
38 | 1, 37 | nfcxfr 2175 |
1
⊢
Ⅎ𝑥Σ𝑘 ∈ 𝐴 𝐵 |