Step | Hyp | Ref
| Expression |
1 | | nfcv 2312 |
. . . 4
⊢
Ⅎ𝑚if(𝑘 ∈ 𝐴, 𝐵, 0) |
2 | | nfv 1521 |
. . . . 5
⊢
Ⅎ𝑘 𝑚 ∈ 𝐴 |
3 | | nfcsb1v 3082 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 |
4 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑘0 |
5 | 2, 3, 4 | nfif 3553 |
. . . 4
⊢
Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0) |
6 | | eleq1w 2231 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴)) |
7 | | csbeq1a 3058 |
. . . . 5
⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵) |
8 | 6, 7 | ifbieq1d 3547 |
. . . 4
⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0)) |
9 | 1, 5, 8 | cbvmpt 4082 |
. . 3
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑚 ∈ ℤ ↦ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 0)) |
10 | | fsumsers.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
11 | 10 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
12 | 3 | nfel1 2323 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ |
13 | 7 | eleq1d 2239 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)) |
14 | 12, 13 | rspc 2828 |
. . . 4
⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)) |
15 | 11, 14 | mpan9 279 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ) |
16 | 6 | dcbid 833 |
. . . 4
⊢ (𝑘 = 𝑚 → (DECID 𝑘 ∈ 𝐴 ↔ DECID 𝑚 ∈ 𝐴)) |
17 | | fsumsers.dc |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴) |
18 | 17 | ralrimiva 2543 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)DECID 𝑘 ∈ 𝐴) |
19 | 18 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ∀𝑘 ∈
(ℤ≥‘𝑀)DECID 𝑘 ∈ 𝐴) |
20 | | simpr 109 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ (ℤ≥‘𝑀)) |
21 | 16, 19, 20 | rspcdva 2839 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → DECID
𝑚 ∈ 𝐴) |
22 | | fsumsers.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
23 | | fsumsers.4 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
24 | 9, 15, 21, 22, 23 | fsum3cvg 11328 |
. 2
⊢ (𝜑 → seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))) ⇝ (seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))‘𝑁)) |
25 | | eluzel2 9479 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
26 | 22, 25 | syl 14 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
27 | | fveq2 5494 |
. . . . 5
⊢ (𝑘 = 𝑥 → (𝐹‘𝑘) = (𝐹‘𝑥)) |
28 | 27 | eleq1d 2239 |
. . . 4
⊢ (𝑘 = 𝑥 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑥) ∈ ℂ)) |
29 | | fsumsers.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
30 | 10 | adantlr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
31 | | 0cnd 7900 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → 0 ∈ ℂ) |
32 | 30, 31, 17 | ifcldadc 3554 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
33 | 29, 32 | eqeltrd 2247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
34 | 33 | ralrimiva 2543 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) |
35 | 34 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ∀𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) |
36 | | simpr 109 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
37 | 28, 35, 36 | rspcdva 2839 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℂ) |
38 | | eluzelz 9483 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
39 | | eqid 2170 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
40 | 39 | fvmpt2 5577 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
41 | 38, 32, 40 | syl2an2 589 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
42 | 29, 41 | eqtr4d 2206 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘)) |
43 | 42 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘)) |
44 | | nffvmpt1 5505 |
. . . . . 6
⊢
Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛) |
45 | 44 | nfeq2 2324 |
. . . . 5
⊢
Ⅎ𝑘(𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛) |
46 | | fveq2 5494 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
47 | | fveq2 5494 |
. . . . . 6
⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛)) |
48 | 46, 47 | eqeq12d 2185 |
. . . . 5
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) ↔ (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛))) |
49 | 45, 48 | rspc 2828 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑘) → (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛))) |
50 | 43, 49 | mpan9 279 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑛) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))‘𝑛)) |
51 | | addcl 7886 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
52 | 51 | adantl 275 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ) |
53 | 26, 37, 50, 52 | seq3feq 10415 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))) |
54 | 53 | fveq1d 5496 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)))‘𝑁)) |
55 | 24, 53, 54 | 3brtr4d 4019 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁)) |