Theorem fsump1

Description: The addition of the next term in a finite sum of A ( k ) is the current term plus B i.e. A ( N + 1 ) . (Contributed by NM, 4-Nov-2005) (Revised by Mario Carneiro, 21-Apr-2014)

	Ref	Expression
Hypotheses	fsump1.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	fsump1.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
	fsump1.3	⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
Assertion	fsump1	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fsump1.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		fsump1.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
3		fsump1.3	⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
4		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
6	5 2 3	fsumm1	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 + 𝐵 ) )
7		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
8	1 7	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9	8	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
10		ax-1cn	⊢ 1 ∈ ℂ
11		pncan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
12	9 10 11	sylancl	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
13	12	oveq2d	⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑀 ... 𝑁 ) )
14	13	sumeq1d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 )
15	14	oveq1d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 + 𝐵 ) = ( Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 + 𝐵 ) )
16	6 15	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 + 𝐵 ) )