Theorem fsump1i

Description: Optimized version of fsump1 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	fsump1i.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	fsump1i.2	⊢ 𝑁 = ( 𝐾 + 1 )
	fsump1i.3	⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐵 )
	fsump1i.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	fsump1i.5	⊢ ( 𝜑 → ( 𝐾 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 = 𝑆 ) )
	fsump1i.6	⊢ ( 𝜑 → ( 𝑆 + 𝐵 ) = 𝑇 )
Assertion	fsump1i	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		fsump1i.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		fsump1i.2	⊢ 𝑁 = ( 𝐾 + 1 )
3		fsump1i.3	⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐵 )
4		fsump1i.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5		fsump1i.5	⊢ ( 𝜑 → ( 𝐾 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 = 𝑆 ) )
6		fsump1i.6	⊢ ( 𝜑 → ( 𝑆 + 𝐵 ) = 𝑇 )
7	5	simpld	⊢ ( 𝜑 → 𝐾 ∈ 𝑍 )
8	7 1	eleqtrdi	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
9		peano2uz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
10	9 1	eleqtrrdi	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 + 1 ) ∈ 𝑍 )
11	8 10	syl	⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ 𝑍 )
12	2 11	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
13	2	oveq2i	⊢ ( 𝑀 ... 𝑁 ) = ( 𝑀 ... ( 𝐾 + 1 ) )
14	13	sumeq1i	⊢ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... ( 𝐾 + 1 ) ) 𝐴
15		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝐾 + 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
16	15 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝐾 + 1 ) ) → 𝑘 ∈ 𝑍 )
17	16 4	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝐾 + 1 ) ) ) → 𝐴 ∈ ℂ )
18	2	eqeq2i	⊢ ( 𝑘 = 𝑁 ↔ 𝑘 = ( 𝐾 + 1 ) )
19	18 3	sylbir	⊢ ( 𝑘 = ( 𝐾 + 1 ) → 𝐴 = 𝐵 )
20	8 17 19	fsump1	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝐾 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 + 𝐵 ) )
21	14 20	eqtrid	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 + 𝐵 ) )
22	5	simprd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 = 𝑆 )
23	22	oveq1d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 + 𝐵 ) = ( 𝑆 + 𝐵 ) )
24	21 23 6	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = 𝑇 )
25	12 24	jca	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = 𝑇 ) )