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

Metamath Proof Explorer

Theorem isum

Description: Series sum with an upper integer index set (i.e. an infinite series). (Contributed by Mario Carneiro, 15-Jul-2013) (Revised by Mario Carneiro, 7-Apr-2014)

Ref Expression
Hypotheses zsum.1 ⊢ Z = ℤ ≥ M
zsum.2 ⊢ φ → M ∈ ℤ
isum.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = B
isum.4 ⊢ φ ∧ k ∈ Z → B ∈ ℂ
Assertion isum ⊢ φ → ∑ k ∈ Z B = ⇝ ⁡ seq M + F

Proof

Step Hyp Ref Expression
1 zsum.1 ⊢ Z = ℤ ≥ M
2 zsum.2 ⊢ φ → M ∈ ℤ
3 isum.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = B
4 isum.4 ⊢ φ ∧ k ∈ Z → B ∈ ℂ
5 ssidd ⊢ φ → Z ⊆ Z
6 iftrue ⊢ k ∈ Z → if k ∈ Z B 0 = B
7 6 adantl ⊢ φ ∧ k ∈ Z → if k ∈ Z B 0 = B
8 3 7 eqtr4d ⊢ φ ∧ k ∈ Z → F ⁡ k = if k ∈ Z B 0
9 1 2 5 8 4 zsum ⊢ φ → ∑ k ∈ Z B = ⇝ ⁡ seq M + F