| Step | Hyp | Ref
| Expression |
| 1 | | df-sum 15723 |
. 2
⊢
Σ𝑘 ∈
𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
| 2 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑘ℤ |
| 3 | | nfsum1.1 |
. . . . . . 7
⊢
Ⅎ𝑘𝐴 |
| 4 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘(ℤ≥‘𝑚) |
| 5 | 3, 4 | nfss 3976 |
. . . . . 6
⊢
Ⅎ𝑘 𝐴 ⊆
(ℤ≥‘𝑚) |
| 6 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑚 |
| 7 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑘
+ |
| 8 | 3 | nfcri 2897 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ 𝐴 |
| 9 | | nfcsb1v 3923 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵 |
| 10 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑘0 |
| 11 | 8, 9, 10 | nfif 4556 |
. . . . . . . . 9
⊢
Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) |
| 12 | 2, 11 | nfmpt 5249 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
| 13 | 6, 7, 12 | nfseq 14052 |
. . . . . . 7
⊢
Ⅎ𝑘seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) |
| 14 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘
⇝ |
| 15 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘𝑥 |
| 16 | 13, 14, 15 | nfbr 5190 |
. . . . . 6
⊢
Ⅎ𝑘seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 |
| 17 | 5, 16 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑘(𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) |
| 18 | 2, 17 | nfrexw 3313 |
. . . 4
⊢
Ⅎ𝑘∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) |
| 19 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑘ℕ |
| 20 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑓 |
| 21 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑘(1...𝑚) |
| 22 | 20, 21, 3 | nff1o 6846 |
. . . . . . 7
⊢
Ⅎ𝑘 𝑓:(1...𝑚)–1-1-onto→𝐴 |
| 23 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑘1 |
| 24 | | nfcsb1v 3923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(𝑓‘𝑛) / 𝑘⦌𝐵 |
| 25 | 19, 24 | nfmpt 5249 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
| 26 | 23, 7, 25 | nfseq 14052 |
. . . . . . . . 9
⊢
Ⅎ𝑘seq1(
+ , (𝑛 ∈ ℕ
↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) |
| 27 | 26, 6 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑘(seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) |
| 28 | 27 | nfeq2 2923 |
. . . . . . 7
⊢
Ⅎ𝑘 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) |
| 29 | 22, 28 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑘(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
| 30 | 29 | nfex 2324 |
. . . . 5
⊢
Ⅎ𝑘∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
| 31 | 19, 30 | nfrexw 3313 |
. . . 4
⊢
Ⅎ𝑘∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
| 32 | 18, 31 | nfor 1904 |
. . 3
⊢
Ⅎ𝑘(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) |
| 33 | 32 | nfiotaw 6518 |
. 2
⊢
Ⅎ𝑘(℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
| 34 | 1, 33 | nfcxfr 2903 |
1
⊢
Ⅎ𝑘Σ𝑘 ∈ 𝐴 𝐵 |