Metamath Proof Explorer

Theorem sersub

Description: The difference of two infinite series. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses sersub.1 ⊢ φ → N ∈ ℤ ≥ M
sersub.2 ⊢ φ ∧ k ∈ M … N → F ⁡ k ∈ ℂ
sersub.3 ⊢ φ ∧ k ∈ M … N → G ⁡ k ∈ ℂ
sersub.4 ⊢ φ ∧ k ∈ M … N → H ⁡ k = F ⁡ k − G ⁡ k
Assertion sersub ⊢ φ → seq M + H ⁡ N = seq M + F ⁡ N − seq M + G ⁡ N

Proof

Step Hyp Ref Expression
1 sersub.1 ⊢ φ → N ∈ ℤ ≥ M
2 sersub.2 ⊢ φ ∧ k ∈ M … N → F ⁡ k ∈ ℂ
3 sersub.3 ⊢ φ ∧ k ∈ M … N → G ⁡ k ∈ ℂ
4 sersub.4 ⊢ φ ∧ k ∈ M … N → H ⁡ k = F ⁡ k − G ⁡ k
5 addcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
6 5 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
7 subcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y ∈ ℂ
8 7 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ → x − y ∈ ℂ
9 addsub4 ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ ∧ w ∈ ℂ → x + y - z + w = x − z + y - w
10 9 eqcomd ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ ∧ w ∈ ℂ → x − z + y - w = x + y - z + w
11 10 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ ∧ w ∈ ℂ → x − z + y - w = x + y - z + w
12 6 8 11 1 2 3 4 seqcaopr2 ⊢ φ → seq M + H ⁡ N = seq M + F ⁡ N − seq M + G ⁡ N