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	$⊢ (φ \land k \in (M \dots N)) \to F (k) = A$
	fsumser.2	$⊢ φ \to N \in ℤ_{\geq M}$
	fsumser.3	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
Assertion	fsumser	$⊢ φ \to \sum_{k = M}^{N} A = seq M (+ F) (N)$

Proof

Step	Hyp	Ref	Expression
1		fsumser.1	$⊢ (φ \land k \in (M \dots N)) \to F (k) = A$
2		fsumser.2	$⊢ φ \to N \in ℤ_{\geq M}$
3		fsumser.3	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
4		eleq1w	$⊢ m = k \to (m \in (M \dots N) \leftrightarrow k \in (M \dots N))$
5		fveq2	$⊢ m = k \to F (m) = F (k)$
6	4 5	ifbieq1d	$⊢ m = k \to if (m \in (M \dots N), F (m), 0) = if (k \in (M \dots N), F (k), 0)$
7		eqid	$⊢ (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0)) = (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0))$
8		fvex	$⊢ F (k) \in V$
9		c0ex	$⊢ 0 \in V$
10	8 9	ifex	$⊢ if (k \in (M \dots N), F (k), 0) \in V$
11	6 7 10	fvmpt	$⊢ k \in ℤ_{\geq M} \to (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0)) (k) = if (k \in (M \dots N), F (k), 0)$
12	1	ifeq1da	$⊢ φ \to if (k \in (M \dots N), F (k), 0) = if (k \in (M \dots N), A, 0)$
13	11 12	sylan9eqr	$⊢ (φ \land k \in ℤ_{\geq M}) \to (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0)) (k) = if (k \in (M \dots N), A, 0)$
14		ssidd	$⊢ φ \to (M \dots N) \subseteq (M \dots N)$
15	13 2 3 14	fsumsers	$⊢ φ \to \sum_{k = M}^{N} A = seq M (+ (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0))) (N)$
16		elfzuz	$⊢ k \in (M \dots N) \to k \in ℤ_{\geq M}$
17	16 11	syl	$⊢ k \in (M \dots N) \to (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0)) (k) = if (k \in (M \dots N), F (k), 0)$
18		iftrue	$⊢ k \in (M \dots N) \to if (k \in (M \dots N), F (k), 0) = F (k)$
19	17 18	eqtrd	$⊢ k \in (M \dots N) \to (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0)) (k) = F (k)$
20	19	adantl	$⊢ (φ \land k \in (M \dots N)) \to (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0)) (k) = F (k)$
21	2 20	seqfveq	$⊢ φ \to seq M (+ (m \in ℤ_{\geq M} ⟼ if (m \in (M \dots N), F (m), 0))) (N) = seq M (+ F) (N)$
22	15 21	eqtrd	$⊢ φ \to \sum_{k = M}^{N} A = seq M (+ F) (N)$

Metamath Proof Explorer

Theorem fsumser

Proof