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

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 ⊢ φ → A ∈ Fin
fsumneg.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
Assertion fsumneg ⊢ φ → ∑ k ∈ A − B = − ∑ k ∈ A B

Proof

Step Hyp Ref Expression
1 fsumneg.1 ⊢ φ → A ∈ Fin
2 fsumneg.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
3 neg1cn ⊢ − 1 ∈ ℂ
4 3 a1i ⊢ φ → − 1 ∈ ℂ
5 1 4 2 fsummulc2 ⊢ φ → -1 ⁢ ∑ k ∈ A B = ∑ k ∈ A -1 ⁢ B
6 1 2 fsumcl ⊢ φ → ∑ k ∈ A B ∈ ℂ
7 6 mulm1d ⊢ φ → -1 ⁢ ∑ k ∈ A B = − ∑ k ∈ A B
8 2 mulm1d ⊢ φ ∧ k ∈ A → -1 ⁢ B = − B
9 8 sumeq2dv ⊢ φ → ∑ k ∈ A -1 ⁢ B = ∑ k ∈ A − B
10 5 7 9 3eqtr3rd ⊢ φ → ∑ k ∈ A − B = − ∑ k ∈ A B