| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. 2
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
| 2 | | sumrb.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 3 | | eluzelz 12888 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
| 4 | 2, 3 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 5 | | seqex 14044 |
. . 3
⊢ seq𝑀( + , 𝐹) ∈ V |
| 6 | 5 | a1i 11 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ V) |
| 7 | | eqid 2737 |
. . . 4
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
| 8 | | eluzel2 12883 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
| 9 | 2, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 10 | | eluzelz 12888 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
| 11 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
| 12 | 11 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
| 13 | | summo.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 14 | 12, 13 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
| 15 | 14 | ex 412 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)) |
| 16 | | iffalse 4534 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
| 17 | | 0cn 11253 |
. . . . . . . 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 7027 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
| 22 | 10, 19, 21 | syl2anr 597 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
| 23 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
| 24 | 22, 23 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
| 25 | 7, 9, 24 | serf 14071 |
. . 3
⊢ (𝜑 → seq𝑀( + , 𝐹):(ℤ≥‘𝑀)⟶ℂ) |
| 26 | 25, 2 | ffvelcdmd 7105 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ) |
| 27 | | addrid 11441 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚) |
| 28 | 27 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚) |
| 29 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 30 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ (ℤ≥‘𝑁)) |
| 31 | 26 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ) |
| 32 | | elfzuz 13560 |
. . . . . 6
⊢ (𝑚 ∈ ((𝑁 + 1)...𝑛) → 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) |
| 33 | | eluzelz 12888 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘(𝑁 + 1)) → 𝑚 ∈ ℤ) |
| 34 | 33 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑚 ∈
ℤ) |
| 35 | | fsumcvg.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
| 36 | 35 | sseld 3982 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑚 ∈ 𝐴 → 𝑚 ∈ (𝑀...𝑁))) |
| 37 | | fznuz 13649 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (𝑀...𝑁) → ¬ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) |
| 38 | 36, 37 | syl6 35 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ 𝐴 → ¬ 𝑚 ∈ (ℤ≥‘(𝑁 + 1)))) |
| 39 | 38 | con2d 134 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ (ℤ≥‘(𝑁 + 1)) → ¬ 𝑚 ∈ 𝐴)) |
| 40 | 39 | imp 406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → ¬ 𝑚 ∈ 𝐴) |
| 41 | 34, 40 | eldifd 3962 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑚 ∈ (ℤ ∖ 𝐴)) |
| 42 | | fveqeq2 6915 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0)) |
| 43 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → 𝑘 ∈ ℤ) |
| 44 | | eldifn 4132 |
. . . . . . . . . . . 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 2777 |
. . . . . . . 8
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑘) = 0) |
| 49 | 42, 48 | vtoclga 3577 |
. . . . . . 7
⊢ (𝑚 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑚) = 0) |
| 50 | 41, 49 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑚) = 0) |
| 51 | 32, 50 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝐹‘𝑚) = 0) |
| 52 | 51 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝐹‘𝑚) = 0) |
| 53 | 28, 29, 30, 31, 52 | seqid2 14089 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐹)‘𝑛)) |
| 54 | 53 | eqcomd 2743 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)) |
| 55 | 1, 4, 6, 26, 54 | climconst 15579 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁)) |