Metamath Proof Explorer

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 syl5eq ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 + 𝐵 ) )
22 5 simprd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 = 𝑆 )
23 22 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 + 𝐵 ) = ( 𝑆 + 𝐵 ) )
24 21 23 6 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = 𝑇 )
25 12 24 jca ⊢ ( 𝜑 → ( 𝑁 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = 𝑇 ) )