Metamath Proof Explorer

Theorem fsumsers

Description: Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 21-Apr-2014)

		Ref	Expression
	Hypotheses	fsumsers.1	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) = if (k \in A, B, 0)$
		fsumsers.2	$⊢ φ \to N \in ℤ_{\geq M}$
		fsumsers.3	$⊢ (φ \land k \in A) \to B \in ℂ$
		fsumsers.4	$⊢ φ \to A \subseteq (M \dots N)$
	Assertion	fsumsers	$⊢ φ \to \sum_{k \in A} B = seq M (+ F) (N)$

Proof

Step	Hyp	Ref	Expression
1		fsumsers.1	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) = if (k \in A, B, 0)$
2		fsumsers.2	$⊢ φ \to N \in ℤ_{\geq M}$
3		fsumsers.3	$⊢ (φ \land k \in A) \to B \in ℂ$
4		fsumsers.4	$⊢ φ \to A \subseteq (M \dots N)$
5		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
6		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
7	2 6	syl	$⊢ φ \to M \in ℤ$
8		fzssuz	$⊢ (M \dots N) \subseteq ℤ_{\geq M}$
9	4 8	sstrdi	$⊢ φ \to A \subseteq ℤ_{\geq M}$
10	5 7 9 1 3	zsum	$⊢ φ \to \sum_{k \in A} B = ⇝ (seq M (+ F))$
11		fclim	$⊢ ⇝ : dom ⇝ ⟶ ℂ$
12		ffun	$⊢ ⇝ : dom ⇝ ⟶ ℂ \to Fun ⇝$
13	11 12	ax-mp	$⊢ Fun ⇝$
14	1 2 3 4	fsumcvg2	$⊢ φ \to seq M (+ F) ⇝ seq M (+ F) (N)$
15		funbrfv	$⊢ Fun ⇝ \to (seq M (+ F) ⇝ seq M (+ F) (N) \to ⇝ (seq M (+ F)) = seq M (+ F) (N))$
16	13 14 15	mpsyl	$⊢ φ \to ⇝ (seq M (+ F)) = seq M (+ F) (N)$
17	10 16	eqtrd	$⊢ φ \to \sum_{k \in A} B = seq M (+ F) (N)$