Theorem isumneg

Description: Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	isumneg.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	isumneg.2	$$⊢\phi \to M\in \mathbb{Z}$$
	isumneg.3	$$⊢\phi \to \sum _{k\in Z}A\in ℂ$$
	isumneg.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	isumneg.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
	isumneg.6	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
Assertion	isumneg	$$⊢\phi \to \sum _{k\in Z}\left(-A\right)=-\sum _{k\in Z}A$$

Proof

Step	Hyp	Ref	Expression
1		isumneg.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumneg.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		isumneg.3	$$⊢\phi \to \sum _{k\in Z}A\in ℂ$$
4		isumneg.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
5		isumneg.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
6		isumneg.6	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
7	5	mulm1d	$$⊢\left(\phi \wedge k\in Z\right)\to -1A=-A$$
8	7	eqcomd	$$⊢\left(\phi \wedge k\in Z\right)\to -A=-1A$$
9	8	sumeq2dv	$$⊢\phi \to \sum _{k\in Z}\left(-A\right)=\sum _{k\in Z}-1A$$
10		1cnd	$$⊢\phi \to 1\in ℂ$$
11	10	negcld	$$⊢\phi \to -1\in ℂ$$
12	1 2 4 5 6 11	isummulc2	$$⊢\phi \to -1\sum _{k\in Z}A=\sum _{k\in Z}-1A$$
13	3	mulm1d	$$⊢\phi \to -1\sum _{k\in Z}A=-\sum _{k\in Z}A$$
14	9 12 13	3eqtr2d	$$⊢\phi \to \sum _{k\in Z}\left(-A\right)=-\sum _{k\in Z}A$$