| Step | Hyp | Ref
| Expression |
| 1 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑚if(𝑘 ∈ 𝐴, 𝐵, 0) |
| 2 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑘 𝑚 ∈ 𝐴 |
| 3 | | nfcsb1v 3923 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 |
| 4 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑘0 |
| 5 | 2, 3, 4 | nfif 4556 |
. . . 4
⊢
Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0) |
| 6 | | eleq1w 2824 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴)) |
| 7 | | csbeq1a 3913 |
. . . . 5
⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵) |
| 8 | 6, 7 | ifbieq1d 4550 |
. . . 4
⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0)) |
| 9 | 1, 5, 8 | cbvmpt 5253 |
. . 3
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑚 ∈ ℤ ↦ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0)) |
| 10 | | fsumsers.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 11 | 10 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
| 12 | 3 | nfel1 2922 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ |
| 13 | 7 | eleq1d 2826 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)) |
| 14 | 12, 13 | rspc 3610 |
. . . 4
⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)) |
| 15 | 11, 14 | mpan9 506 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ) |
| 16 | | fsumsers.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 17 | | fsumsers.4 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
| 18 | 9, 15, 16, 17 | fsumcvg 15748 |
. 2
⊢ (𝜑 → seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))) ⇝ (seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))‘𝑁)) |
| 19 | | eluzel2 12883 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
| 20 | 16, 19 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 21 | | fsumsers.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
| 22 | | eluzelz 12888 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
| 23 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
| 24 | 23 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
| 25 | 24, 10 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
| 26 | 25 | ex 412 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)) |
| 27 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
| 28 | | 0cn 11253 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
| 29 | 27, 28 | eqeltrdi 2849 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
| 30 | 26, 29 | pm2.61d1 180 |
. . . . . . 7
⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
| 31 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
| 32 | 31 | fvmpt2 7027 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
| 33 | 22, 30, 32 | syl2anr 597 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
| 34 | 21, 33 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘)) |
| 35 | 34 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘)) |
| 36 | | nffvmpt1 6917 |
. . . . . 6
⊢
Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛) |
| 37 | 36 | nfeq2 2923 |
. . . . 5
⊢
Ⅎ𝑘(𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛) |
| 38 | | fveq2 6906 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
| 39 | | fveq2 6906 |
. . . . . 6
⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛)) |
| 40 | 38, 39 | eqeq12d 2753 |
. . . . 5
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) ↔ (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛))) |
| 41 | 37, 40 | rspc 3610 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) → (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛))) |
| 42 | 35, 41 | mpan9 506 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛)) |
| 43 | 20, 42 | seqfeq 14068 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))) |
| 44 | 43 | fveq1d 6908 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))‘𝑁)) |
| 45 | 18, 43, 44 | 3brtr4d 5175 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁)) |