Step | Hyp | Ref
| Expression |
1 | | nfcv 2907 |
. . . 4
⊢
Ⅎ𝑚if(𝑘 ∈ 𝐴, 𝐵, 0) |
2 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑘 𝑚 ∈ 𝐴 |
3 | | nfcsb1v 3857 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 |
4 | | nfcv 2907 |
. . . . 5
⊢
Ⅎ𝑘0 |
5 | 2, 3, 4 | nfif 4489 |
. . . 4
⊢
Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0) |
6 | | eleq1w 2821 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴)) |
7 | | csbeq1a 3846 |
. . . . 5
⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵) |
8 | 6, 7 | ifbieq1d 4483 |
. . . 4
⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0)) |
9 | 1, 5, 8 | cbvmpt 5185 |
. . 3
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑚 ∈ ℤ ↦ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0)) |
10 | | fsumsers.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
11 | 10 | ralrimiva 3103 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
12 | 3 | nfel1 2923 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ |
13 | 7 | eleq1d 2823 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)) |
14 | 12, 13 | rspc 3549 |
. . . 4
⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)) |
15 | 11, 14 | mpan9 507 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ) |
16 | | fsumsers.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
17 | | fsumsers.4 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
18 | 9, 15, 16, 17 | fsumcvg 15424 |
. 2
⊢ (𝜑 → seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))) ⇝ (seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))‘𝑁)) |
19 | | eluzel2 12587 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
20 | 16, 19 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
21 | | fsumsers.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
22 | | eluzelz 12592 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
23 | | iftrue 4465 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
24 | 23 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
25 | 24, 10 | eqeltrd 2839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
26 | 25 | ex 413 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)) |
27 | | iffalse 4468 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
28 | | 0cn 10967 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
29 | 27, 28 | eqeltrdi 2847 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
30 | 26, 29 | pm2.61d1 180 |
. . . . . . 7
⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
31 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
32 | 31 | fvmpt2 6886 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
33 | 22, 30, 32 | syl2anr 597 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
34 | 21, 33 | eqtr4d 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘)) |
35 | 34 | ralrimiva 3103 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘)) |
36 | | nffvmpt1 6785 |
. . . . . 6
⊢
Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛) |
37 | 36 | nfeq2 2924 |
. . . . 5
⊢
Ⅎ𝑘(𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛) |
38 | | fveq2 6774 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
39 | | fveq2 6774 |
. . . . . 6
⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛)) |
40 | 38, 39 | eqeq12d 2754 |
. . . . 5
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) ↔ (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛))) |
41 | 37, 40 | rspc 3549 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) → (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛))) |
42 | 35, 41 | mpan9 507 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛)) |
43 | 20, 42 | seqfeq 13748 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))) |
44 | 43 | fveq1d 6776 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))‘𝑁)) |
45 | 18, 43, 44 | 3brtr4d 5106 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁)) |