Theorem fsumneg

Description: Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	fsumneg.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumneg.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
Assertion	fsumneg	$$⊢\phi \to \sum _{k\in A}\left(-B\right)=-\sum _{k\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		fsumneg.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumneg.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
3		neg1cn	$$⊢-1\in ℂ$$
4	3	a1i	$$⊢\phi \to -1\in ℂ$$
5	1 4 2	fsummulc2	$$⊢\phi \to -1\sum _{k\in A}B=\sum _{k\in A}-1B$$
6	1 2	fsumcl	$$⊢\phi \to \sum _{k\in A}B\in ℂ$$
7	6	mulm1d	$$⊢\phi \to -1\sum _{k\in A}B=-\sum _{k\in A}B$$
8	2	mulm1d	$$⊢\left(\phi \wedge k\in A\right)\to -1B=-B$$
9	8	sumeq2dv	$$⊢\phi \to \sum _{k\in A}-1B=\sum _{k\in A}\left(-B\right)$$
10	5 7 9	3eqtr3rd	$$⊢\phi \to \sum _{k\in A}\left(-B\right)=-\sum _{k\in A}B$$