This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )