seradd

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

Step	Hyp	Ref	Expression
1		seradd.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		seradd.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℂ$
3		seradd.3	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in ℂ$
4		seradd.4	$⊢ (φ \land k \in (M \dots N)) \to H (k) = F (k) + G (k)$
5		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
6	5	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x + y \in ℂ$
7		addcom	$⊢ (x \in ℂ \land y \in ℂ) \to x + y = y + x$
8	7	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x + y = y + x$
9		addass	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x + y + z = x + y + z$
10	9	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to x + y + z = x + y + z$
11	6 8 10 1 2 3 4	seqcaopr	$⊢ φ \to seq M (+ H) (N) = seq M (+ F) (N) + seq M (+ G) (N)$

Metamath Proof Explorer