Metamath Proof Explorer

Theorem seradd

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

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

Proof

Step Hyp Ref Expression
1 seradd.1 ⊢ φ → N ∈ ℤ ≥ M
2 seradd.2 ⊢ φ ∧ k ∈ M … N → F ⁡ k ∈ ℂ
3 seradd.3 ⊢ φ ∧ k ∈ M … N → G ⁡ k ∈ ℂ
4 seradd.4 ⊢ φ ∧ k ∈ M … N → H ⁡ k = F ⁡ k + G ⁡ k
5 addcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
6 5 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
7 addcom ⊢ x ∈ ℂ ∧ y ∈ ℂ → x + y = y + x
8 7 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ → x + y = y + x
9 addass ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → x + y + z = x + y + z
10 9 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → x + y + z = x + y + z
11 6 8 10 1 2 3 4 seqcaopr ⊢ φ → seq M + H ⁡ N = seq M + F ⁡ N + seq M + G ⁡ N