Metamath Proof Explorer

Theorem fsumcvg2

Description: The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014)

Ref Expression
Hypotheses fsumsers.1 ⊢φ∧k∈ℤ≥M→F⁡k=ifk∈AB0
fsumsers.2 ⊢φ→N∈ℤ≥M
fsumsers.3 ⊢φ∧k∈A→B∈ℂ
fsumsers.4 ⊢φ→A⊆M…N
Assertion fsumcvg2 ⊢φ→seqM+F⇝seqM+F⁡N

Proof

Step Hyp Ref Expression
1 fsumsers.1 ⊢φ∧k∈ℤ≥M→F⁡k=ifk∈AB0
2 fsumsers.2 ⊢φ→N∈ℤ≥M
3 fsumsers.3 ⊢φ∧k∈A→B∈ℂ
4 fsumsers.4 ⊢φ→A⊆M…N
5 nfcv ⊢Ⅎ_mifk∈AB0
6 nfv ⊢Ⅎkm∈A
7 nfcsb1v ⊢Ⅎ_k⦋m/k⦌B
8 nfcv ⊢Ⅎ_k0
9 6 7 8 nfif ⊢Ⅎ_kifm∈A⦋m/k⦌B0
10 eleq1w ⊢k=m→k∈A↔m∈A
11 csbeq1a ⊢k=m→B=⦋m/k⦌B
12 10 11 ifbieq1d ⊢k=m→ifk∈AB0=ifm∈A⦋m/k⦌B0
13 5 9 12 cbvmpt ⊢k∈ℤ⟼ifk∈AB0=m∈ℤ⟼ifm∈A⦋m/k⦌B0
14 3 ralrimiva ⊢φ→∀k∈AB∈ℂ
15 7 nfel1 ⊢Ⅎk⦋m/k⦌B∈ℂ
16 11 eleq1d ⊢k=m→B∈ℂ↔⦋m/k⦌B∈ℂ
17 15 16 rspc ⊢m∈A→∀k∈AB∈ℂ→⦋m/k⦌B∈ℂ
18 14 17 mpan9 ⊢φ∧m∈A→⦋m/k⦌B∈ℂ
19 13 18 2 4 fsumcvg ⊢φ→seqM+k∈ℤ⟼ifk∈AB0⇝seqM+k∈ℤ⟼ifk∈AB0⁡N
20 eluzel2 ⊢N∈ℤ≥M→M∈ℤ
21 2 20 syl ⊢φ→M∈ℤ
22 eluzelz ⊢k∈ℤ≥M→k∈ℤ
23 iftrue ⊢k∈A→ifk∈AB0=B
24 23 adantl ⊢φ∧k∈A→ifk∈AB0=B
25 24 3 eqeltrd ⊢φ∧k∈A→ifk∈AB0∈ℂ
26 25 ex ⊢φ→k∈A→ifk∈AB0∈ℂ
27 iffalse ⊢¬k∈A→ifk∈AB0=0
28 0cn ⊢0∈ℂ
29 27 28 eqeltrdi ⊢¬k∈A→ifk∈AB0∈ℂ
30 26 29 pm2.61d1 ⊢φ→ifk∈AB0∈ℂ
31 eqid ⊢k∈ℤ⟼ifk∈AB0=k∈ℤ⟼ifk∈AB0
32 31 fvmpt2 ⊢k∈ℤ∧ifk∈AB0∈ℂ→k∈ℤ⟼ifk∈AB0⁡k=ifk∈AB0
33 22 30 32 syl2anr ⊢φ∧k∈ℤ≥M→k∈ℤ⟼ifk∈AB0⁡k=ifk∈AB0
34 1 33 eqtr4d ⊢φ∧k∈ℤ≥M→F⁡k=k∈ℤ⟼ifk∈AB0⁡k
35 34 ralrimiva ⊢φ→∀k∈ℤ≥MF⁡k=k∈ℤ⟼ifk∈AB0⁡k
36 nffvmpt1 ⊢Ⅎ_kk∈ℤ⟼ifk∈AB0⁡n
37 36 nfeq2 ⊢ℲkF⁡n=k∈ℤ⟼ifk∈AB0⁡n
38 fveq2 ⊢k=n→F⁡k=F⁡n
39 fveq2 ⊢k=n→k∈ℤ⟼ifk∈AB0⁡k=k∈ℤ⟼ifk∈AB0⁡n
40 38 39 eqeq12d ⊢k=n→F⁡k=k∈ℤ⟼ifk∈AB0⁡k↔F⁡n=k∈ℤ⟼ifk∈AB0⁡n
41 37 40 rspc ⊢n∈ℤ≥M→∀k∈ℤ≥MF⁡k=k∈ℤ⟼ifk∈AB0⁡k→F⁡n=k∈ℤ⟼ifk∈AB0⁡n
42 35 41 mpan9 ⊢φ∧n∈ℤ≥M→F⁡n=k∈ℤ⟼ifk∈AB0⁡n
43 21 42 seqfeq ⊢φ→seqM+F=seqM+k∈ℤ⟼ifk∈AB0
44 43 fveq1d ⊢φ→seqM+F⁡N=seqM+k∈ℤ⟼ifk∈AB0⁡N
45 19 43 44 3brtr4d ⊢φ→seqM+F⇝seqM+F⁡N