sersub

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

Step	Hyp	Ref	Expression
1		sersub.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		sersub.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℂ$
3		sersub.3	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in ℂ$
4		sersub.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		subcl	$⊢ (x \in ℂ \land y \in ℂ) \to x - y \in ℂ$
8	7	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x - y \in ℂ$
9		addsub4	$⊢ ((x \in ℂ \land y \in ℂ) \land (z \in ℂ \land w \in ℂ)) \to x + y - (z + w) = (x - z) + y - w$
10	9	eqcomd	$⊢ ((x \in ℂ \land y \in ℂ) \land (z \in ℂ \land w \in ℂ)) \to (x - z) + y - w = x + y - (z + w)$
11	10	adantl	$⊢ (φ \land ((x \in ℂ \land y \in ℂ) \land (z \in ℂ \land w \in ℂ))) \to (x - z) + y - w = x + y - (z + w)$
12	6 8 11 1 2 3 4	seqcaopr2	$⊢ φ \to seq M (+ H) (N) = seq M (+ F) (N) - seq M (+ G) (N)$

Metamath Proof Explorer