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	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
	fsumsers.2	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	fsumsers.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fsumsers.4	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
Assertion	fsumsers	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fsumsers.1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
2		fsumsers.2	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3		fsumsers.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4		fsumsers.4	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
5		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
6		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
7	2 6	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8		fzssuz	⊢ ( 𝑀 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 )
9	4 8	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
10	5 7 9 1 3	zsum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
11		fclim	⊢ ⇝ : dom ⇝ ⟶ ℂ
12		ffun	⊢ ( ⇝ : dom ⇝ ⟶ ℂ → Fun ⇝ )
13	11 12	ax-mp	⊢ Fun ⇝
14	1 2 3 4	fsumcvg2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
15		funbrfv	⊢ ( Fun ⇝ → ( seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
16	13 14 15	mpsyl	⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
17	10 16	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )