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

Metamath Proof Explorer

Theorem fsumsub

Description: Split a finite sum over a subtraction. (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 ∈ ℂ
fsumsub.3 ⊢ φ ∧ k ∈ A → C ∈ ℂ
Assertion fsumsub ⊢ φ → ∑ k ∈ A B − C = ∑ k ∈ A B − ∑ k ∈ A C

Proof

Step Hyp Ref Expression
1 fsumneg.1 ⊢ φ → A ∈ Fin
2 fsumneg.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
3 fsumsub.3 ⊢ φ ∧ k ∈ A → C ∈ ℂ
4 3 negcld ⊢ φ ∧ k ∈ A → − C ∈ ℂ
5 1 2 4 fsumadd ⊢ φ → ∑ k ∈ A B + − C = ∑ k ∈ A B + ∑ k ∈ A − C
6 1 3 fsumneg ⊢ φ → ∑ k ∈ A − C = − ∑ k ∈ A C
7 6 oveq2d ⊢ φ → ∑ k ∈ A B + ∑ k ∈ A − C = ∑ k ∈ A B + − ∑ k ∈ A C
8 5 7 eqtrd ⊢ φ → ∑ k ∈ A B + − C = ∑ k ∈ A B + − ∑ k ∈ A C
9 2 3 negsubd ⊢ φ ∧ k ∈ A → B + − C = B − C
10 9 sumeq2dv ⊢ φ → ∑ k ∈ A B + − C = ∑ k ∈ A B − C
11 1 2 fsumcl ⊢ φ → ∑ k ∈ A B ∈ ℂ
12 1 3 fsumcl ⊢ φ → ∑ k ∈ A C ∈ ℂ
13 11 12 negsubd ⊢ φ → ∑ k ∈ A B + − ∑ k ∈ A C = ∑ k ∈ A B − ∑ k ∈ A C
14 8 10 13 3eqtr3d ⊢ φ → ∑ k ∈ A B − C = ∑ k ∈ A B − ∑ k ∈ A C