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 = if k ∈ A B 0
fsumsers.2 ⊢ φ → N ∈ ℤ ≥ M
fsumsers.3 ⊢ φ ∧ k ∈ A → B ∈ ℂ
fsumsers.4 ⊢ φ → A ⊆ M … N
Assertion fsumcvg2 ⊢ φ → seq M + F ⇝ seq M + F ⁡ N

Proof

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