Step | Hyp | Ref
| Expression |
1 | | eqid 2740 |
. 2
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
2 | | sumrb.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
3 | | eluzelz 12583 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
4 | 2, 3 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℤ) |
5 | | seqex 13713 |
. . 3
⊢ seq𝑀( + , 𝐹) ∈ V |
6 | 5 | a1i 11 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ V) |
7 | | eqid 2740 |
. . . 4
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
8 | | eluzel2 12578 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
9 | 2, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
10 | | eluzelz 12583 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
11 | | iftrue 4471 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
12 | 11 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
13 | | summo.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
14 | 12, 13 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
15 | 14 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)) |
16 | | iffalse 4474 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
17 | | 0cn 10960 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
18 | 16, 17 | eqeltrdi 2849 |
. . . . . . 7
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
19 | 15, 18 | pm2.61d1 180 |
. . . . . 6
⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
20 | | summo.1 |
. . . . . . 7
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
21 | 20 | fvmpt2 6881 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
22 | 10, 19, 21 | syl2anr 597 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
23 | 19 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
24 | 22, 23 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
25 | 7, 9, 24 | serf 13741 |
. . 3
⊢ (𝜑 → seq𝑀( + , 𝐹):(ℤ≥‘𝑀)⟶ℂ) |
26 | 25, 2 | ffvelrnd 6957 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ) |
27 | | addid1 11147 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚) |
28 | 27 | adantl 482 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚) |
29 | 2 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
30 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ (ℤ≥‘𝑁)) |
31 | 26 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ) |
32 | | elfzuz 13243 |
. . . . . 6
⊢ (𝑚 ∈ ((𝑁 + 1)...𝑛) → 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) |
33 | | eluzelz 12583 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘(𝑁 + 1)) → 𝑚 ∈ ℤ) |
34 | 33 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑚 ∈
ℤ) |
35 | | fsumcvg.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
36 | 35 | sseld 3925 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑚 ∈ 𝐴 → 𝑚 ∈ (𝑀...𝑁))) |
37 | | fznuz 13329 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (𝑀...𝑁) → ¬ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) |
38 | 36, 37 | syl6 35 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ 𝐴 → ¬ 𝑚 ∈ (ℤ≥‘(𝑁 + 1)))) |
39 | 38 | con2d 134 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ (ℤ≥‘(𝑁 + 1)) → ¬ 𝑚 ∈ 𝐴)) |
40 | 39 | imp 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → ¬ 𝑚 ∈ 𝐴) |
41 | 34, 40 | eldifd 3903 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑚 ∈ (ℤ ∖ 𝐴)) |
42 | | fveqeq2 6778 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0)) |
43 | | eldifi 4066 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → 𝑘 ∈ ℤ) |
44 | | eldifn 4067 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
45 | 44, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
46 | 45, 17 | eqeltrdi 2849 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
47 | 43, 46, 21 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
48 | 47, 45 | eqtrd 2780 |
. . . . . . . 8
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑘) = 0) |
49 | 42, 48 | vtoclga 3512 |
. . . . . . 7
⊢ (𝑚 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑚) = 0) |
50 | 41, 49 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑚) = 0) |
51 | 32, 50 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝐹‘𝑚) = 0) |
52 | 51 | adantlr 712 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝐹‘𝑚) = 0) |
53 | 28, 29, 30, 31, 52 | seqid2 13759 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐹)‘𝑛)) |
54 | 53 | eqcomd 2746 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)) |
55 | 1, 4, 6, 26, 54 | climconst 15242 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁)) |