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