Metamath Proof Explorer

Theorem isum1p

Description: The infinite sum of a converging infinite series equals the first term plus the infinite sum of the rest of it. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isum1p.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isum1p.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isum1p.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
isum1p.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
isum1p.6 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion isum1p ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ( 𝐹 ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isum1p.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isum1p.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 isum1p.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4 isum1p.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5 isum1p.6 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6 eqid ⊢ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) = ( ℤ≥ ‘ ( 𝑀 + 1 ) )
7 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 2 7 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
10 8 9 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
11 10 1 eleqtrrdi ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ 𝑍 )
12 1 6 11 3 4 5 isumsplit ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑀 + 1 ) − 1 ) ) 𝐴 + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) 𝐴 ) )
13 2 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
14 ax-1cn ⊢ 1 ∈ ℂ
15 pncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
16 13 14 15 sylancl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
17 16 oveq2d ⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝑀 + 1 ) − 1 ) ) = ( 𝑀 ... 𝑀 ) )
18 17 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑀 + 1 ) − 1 ) ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 )
19 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
20 19 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) → 𝑘 ∈ 𝑍 )
21 20 3 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
22 21 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 )
23 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
24 23 eleq1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑀 ) ∈ ℂ ) )
25 3 4 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
26 25 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
27 8 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
28 24 26 27 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℂ )
29 23 fsum1 ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐹 ‘ 𝑀 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
30 2 28 29 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
31 18 22 30 3eqtr2d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑀 + 1 ) − 1 ) ) 𝐴 = ( 𝐹 ‘ 𝑀 ) )
32 31 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑀 + 1 ) − 1 ) ) 𝐴 + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) 𝐴 ) = ( ( 𝐹 ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) 𝐴 ) )
33 12 32 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ( 𝐹 ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) 𝐴 ) )