Metamath Proof Explorer

Theorem fsumser

Description: A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 and fsump1i , which should make our notation clear and from which, along with closure fsumcl , we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 21-Apr-2014)

Ref Expression
Hypotheses fsumser.1 ⊢ φ ∧ k ∈ M … N → F ⁡ k = A
fsumser.2 ⊢ φ → N ∈ ℤ ≥ M
fsumser.3 ⊢ φ ∧ k ∈ M … N → A ∈ ℂ
Assertion fsumser ⊢ φ → ∑ k = M N A = seq M + F ⁡ N

Proof

Step Hyp Ref Expression
1 fsumser.1 ⊢ φ ∧ k ∈ M … N → F ⁡ k = A
2 fsumser.2 ⊢ φ → N ∈ ℤ ≥ M
3 fsumser.3 ⊢ φ ∧ k ∈ M … N → A ∈ ℂ
4 eleq1w ⊢ m = k → m ∈ M … N ↔ k ∈ M … N
5 fveq2 ⊢ m = k → F ⁡ m = F ⁡ k
6 4 5 ifbieq1d ⊢ m = k → if m ∈ M … N F ⁡ m 0 = if k ∈ M … N F ⁡ k 0
7 eqid ⊢ m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0 = m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0
8 fvex ⊢ F ⁡ k ∈ V
9 c0ex ⊢ 0 ∈ V
10 8 9 ifex ⊢ if k ∈ M … N F ⁡ k 0 ∈ V
11 6 7 10 fvmpt ⊢ k ∈ ℤ ≥ M → m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0 ⁡ k = if k ∈ M … N F ⁡ k 0
12 1 ifeq1da ⊢ φ → if k ∈ M … N F ⁡ k 0 = if k ∈ M … N A 0
13 11 12 sylan9eqr ⊢ φ ∧ k ∈ ℤ ≥ M → m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0 ⁡ k = if k ∈ M … N A 0
14 ssidd ⊢ φ → M … N ⊆ M … N
15 13 2 3 14 fsumsers ⊢ φ → ∑ k = M N A = seq M + m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0 ⁡ N
16 elfzuz ⊢ k ∈ M … N → k ∈ ℤ ≥ M
17 16 11 syl ⊢ k ∈ M … N → m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0 ⁡ k = if k ∈ M … N F ⁡ k 0
18 iftrue ⊢ k ∈ M … N → if k ∈ M … N F ⁡ k 0 = F ⁡ k
19 17 18 eqtrd ⊢ k ∈ M … N → m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0 ⁡ k = F ⁡ k
20 19 adantl ⊢ φ ∧ k ∈ M … N → m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0 ⁡ k = F ⁡ k
21 2 20 seqfveq ⊢ φ → seq M + m ∈ ℤ ≥ M ⟼ if m ∈ M … N F ⁡ m 0 ⁡ N = seq M + F ⁡ N
22 15 21 eqtrd ⊢ φ → ∑ k = M N A = seq M + F ⁡ N