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

Proof

Step	Hyp	Ref	Expression
1		fsumser.1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
2		fsumser.2	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3		fsumser.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
4		eleq1w	⊢ ( 𝑚 = 𝑘 → ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) )
5		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
6	4 5	ifbieq1d	⊢ ( 𝑚 = 𝑘 → if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) = if ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑘 ) , 0 ) )
7		eqid	⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) )
8		fvex	⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
9		c0ex	⊢ 0 ∈ V
10	8 9	ifex	⊢ if ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑘 ) , 0 ) ∈ V
11	6 7 10	fvmpt	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑘 ) , 0 ) )
12	1	ifeq1da	⊢ ( 𝜑 → if ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑘 ) , 0 ) = if ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) , 𝐴 , 0 ) )
13	11 12	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) , 𝐴 , 0 ) )
14		ssidd	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
15	13 2 3 14	fsumsers	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( seq 𝑀 ( + , ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) ) ) ‘ 𝑁 ) )
16		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
17	16 11	syl	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑘 ) , 0 ) )
18		iftrue	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → if ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑘 ) , 0 ) = ( 𝐹 ‘ 𝑘 ) )
19	17 18	eqtrd	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
21	2 20	seqfveq	⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) , ( 𝐹 ‘ 𝑚 ) , 0 ) ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
22	15 21	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )