# 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 ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑘 ) = 𝐴 )
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 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )