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={\mathbb{Z}}_{\ge M}$$
	zsum.2	$$⊢\phi \to M\in \mathbb{Z}$$
	isum.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
	isum.4	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
Assertion	isum	$$⊢\phi \to \sum _{k\in Z}B=⇝\left(seqM\left(+,F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		zsum.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		zsum.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		isum.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
4		isum.4	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
5		ssidd	$$⊢\phi \to Z\subseteq Z$$
6		iftrue	$$⊢k\in Z\to if\left(k\in Z,B,0\right)=B$$
7	6	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to if\left(k\in Z,B,0\right)=B$$
8	3 7	eqtr4d	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=if\left(k\in Z,B,0\right)$$
9	1 2 5 8 4	zsum	$$⊢\phi \to \sum _{k\in Z}B=⇝\left(seqM\left(+,F\right)\right)$$