Metamath Proof Explorer


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
|- ( ph -> A e. Fin )
fsumneg.2
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsumneg
|- ( ph -> sum_ k e. A -u B = -u sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 fsumneg.1
 |-  ( ph -> A e. Fin )
2 fsumneg.2
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 neg1cn
 |-  -u 1 e. CC
4 3 a1i
 |-  ( ph -> -u 1 e. CC )
5 1 4 2 fsummulc2
 |-  ( ph -> ( -u 1 x. sum_ k e. A B ) = sum_ k e. A ( -u 1 x. B ) )
6 1 2 fsumcl
 |-  ( ph -> sum_ k e. A B e. CC )
7 6 mulm1d
 |-  ( ph -> ( -u 1 x. sum_ k e. A B ) = -u sum_ k e. A B )
8 2 mulm1d
 |-  ( ( ph /\ k e. A ) -> ( -u 1 x. B ) = -u B )
9 8 sumeq2dv
 |-  ( ph -> sum_ k e. A ( -u 1 x. B ) = sum_ k e. A -u B )
10 5 7 9 3eqtr3rd
 |-  ( ph -> sum_ k e. A -u B = -u sum_ k e. A B )