Step | Hyp | Ref
| Expression |
1 | | nfcv 2900 |
. . . 4
⊢
Ⅎ𝑚if(𝑘 ∈ 𝐴, 𝐵, 0) |
2 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑘 𝑚 ∈ 𝐴 |
3 | | nfcsb1v 3824 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 |
4 | | nfcv 2900 |
. . . . 5
⊢
Ⅎ𝑘0 |
5 | 2, 3, 4 | nfif 4454 |
. . . 4
⊢
Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0) |
6 | | eleq1w 2816 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴)) |
7 | | csbeq1a 3814 |
. . . . 5
⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵) |
8 | 6, 7 | ifbieq1d 4448 |
. . . 4
⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0)) |
9 | 1, 5, 8 | cbvmpt 5141 |
. . 3
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑚 ∈ ℤ ↦ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0)) |
10 | | fsumsers.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
11 | 10 | ralrimiva 3097 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
12 | 3 | nfel1 2916 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ |
13 | 7 | eleq1d 2818 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)) |
14 | 12, 13 | rspc 3517 |
. . . 4
⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)) |
15 | 11, 14 | mpan9 510 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ) |
16 | | fsumsers.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
17 | | fsumsers.4 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
18 | 9, 15, 16, 17 | fsumcvg 15174 |
. 2
⊢ (𝜑 → seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))) ⇝ (seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))‘𝑁)) |
19 | | eluzel2 12341 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
20 | 16, 19 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
21 | | fsumsers.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
22 | | eluzelz 12346 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
23 | | iftrue 4430 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
24 | 23 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
25 | 24, 10 | eqeltrd 2834 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
26 | 25 | ex 416 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)) |
27 | | iffalse 4433 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
28 | | 0cn 10723 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
29 | 27, 28 | eqeltrdi 2842 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
30 | 26, 29 | pm2.61d1 183 |
. . . . . . 7
⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
31 | | eqid 2739 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
32 | 31 | fvmpt2 6798 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
33 | 22, 30, 32 | syl2anr 600 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
34 | 21, 33 | eqtr4d 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘)) |
35 | 34 | ralrimiva 3097 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘)) |
36 | | nffvmpt1 6697 |
. . . . . 6
⊢
Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛) |
37 | 36 | nfeq2 2917 |
. . . . 5
⊢
Ⅎ𝑘(𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛) |
38 | | fveq2 6686 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
39 | | fveq2 6686 |
. . . . . 6
⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛)) |
40 | 38, 39 | eqeq12d 2755 |
. . . . 5
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) ↔ (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛))) |
41 | 37, 40 | rspc 3517 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) → (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛))) |
42 | 35, 41 | mpan9 510 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛)) |
43 | 20, 42 | seqfeq 13499 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))) |
44 | 43 | fveq1d 6688 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))‘𝑁)) |
45 | 18, 43, 44 | 3brtr4d 5072 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁)) |