seqcaopr

Description: The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 30-May-2014)

	Ref	Expression
Hypotheses	seqcaopr.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqcaopr.2	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
	seqcaopr.3	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	seqcaopr.4	$⊢ φ \to N \in ℤ_{\geq M}$
	seqcaopr.5	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in S$
	seqcaopr.6	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in S$
	seqcaopr.7	$⊢ (φ \land k \in (M \dots N)) \to H (k) = F (k) \underset{˙}{+} G (k)$
Assertion	seqcaopr	$⊢ φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, F) (N) \underset{˙}{+} seq M (\underset{˙}{+}, G) (N)$

Proof

Step	Hyp	Ref	Expression
1		seqcaopr.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
2		seqcaopr.2	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
3		seqcaopr.3	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
4		seqcaopr.4	$⊢ φ \to N \in ℤ_{\geq M}$
5		seqcaopr.5	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in S$
6		seqcaopr.6	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in S$
7		seqcaopr.7	$⊢ (φ \land k \in (M \dots N)) \to H (k) = F (k) \underset{˙}{+} G (k)$
8	1	caovclg	$⊢ (φ \land (a \in S \land b \in S)) \to a \underset{˙}{+} b \in S$
9		simpl	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to φ$
10		simprrl	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to c \in S$
11		simprlr	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to b \in S$
12	2	caovcomg	$⊢ (φ \land (c \in S \land b \in S)) \to c \underset{˙}{+} b = b \underset{˙}{+} c$
13	9 10 11 12	syl12anc	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to c \underset{˙}{+} b = b \underset{˙}{+} c$
14	13	oveq1d	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to (c \underset{˙}{+} b) \underset{˙}{+} d = (b \underset{˙}{+} c) \underset{˙}{+} d$
15		simprrr	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to d \in S$
16	3	caovassg	$⊢ (φ \land (c \in S \land b \in S \land d \in S)) \to (c \underset{˙}{+} b) \underset{˙}{+} d = c \underset{˙}{+} (b \underset{˙}{+} d)$
17	9 10 11 15 16	syl13anc	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to (c \underset{˙}{+} b) \underset{˙}{+} d = c \underset{˙}{+} (b \underset{˙}{+} d)$
18	3	caovassg	$⊢ (φ \land (b \in S \land c \in S \land d \in S)) \to (b \underset{˙}{+} c) \underset{˙}{+} d = b \underset{˙}{+} (c \underset{˙}{+} d)$
19	9 11 10 15 18	syl13anc	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to (b \underset{˙}{+} c) \underset{˙}{+} d = b \underset{˙}{+} (c \underset{˙}{+} d)$
20	14 17 19	3eqtr3d	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to c \underset{˙}{+} (b \underset{˙}{+} d) = b \underset{˙}{+} (c \underset{˙}{+} d)$
21	20	oveq2d	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to a \underset{˙}{+} (c \underset{˙}{+} (b \underset{˙}{+} d)) = a \underset{˙}{+} (b \underset{˙}{+} (c \underset{˙}{+} d))$
22		simprll	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to a \in S$
23	1	caovclg	$⊢ (φ \land (b \in S \land d \in S)) \to b \underset{˙}{+} d \in S$
24	9 11 15 23	syl12anc	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to b \underset{˙}{+} d \in S$
25	3	caovassg	$⊢ (φ \land (a \in S \land c \in S \land b \underset{˙}{+} d \in S)) \to (a \underset{˙}{+} c) \underset{˙}{+} (b \underset{˙}{+} d) = a \underset{˙}{+} (c \underset{˙}{+} (b \underset{˙}{+} d))$
26	9 22 10 24 25	syl13anc	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to (a \underset{˙}{+} c) \underset{˙}{+} (b \underset{˙}{+} d) = a \underset{˙}{+} (c \underset{˙}{+} (b \underset{˙}{+} d))$
27	1	caovclg	$⊢ (φ \land (c \in S \land d \in S)) \to c \underset{˙}{+} d \in S$
28	27	adantrl	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to c \underset{˙}{+} d \in S$
29	3	caovassg	$⊢ (φ \land (a \in S \land b \in S \land c \underset{˙}{+} d \in S)) \to (a \underset{˙}{+} b) \underset{˙}{+} (c \underset{˙}{+} d) = a \underset{˙}{+} (b \underset{˙}{+} (c \underset{˙}{+} d))$
30	9 22 11 28 29	syl13anc	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to (a \underset{˙}{+} b) \underset{˙}{+} (c \underset{˙}{+} d) = a \underset{˙}{+} (b \underset{˙}{+} (c \underset{˙}{+} d))$
31	21 26 30	3eqtr4d	$⊢ (φ \land ((a \in S \land b \in S) \land (c \in S \land d \in S))) \to (a \underset{˙}{+} c) \underset{˙}{+} (b \underset{˙}{+} d) = (a \underset{˙}{+} b) \underset{˙}{+} (c \underset{˙}{+} d)$
32	8 8 31 4 5 6 7	seqcaopr2	$⊢ φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, F) (N) \underset{˙}{+} seq M (\underset{˙}{+}, G) (N)$

Metamath Proof Explorer

Theorem seqcaopr

Proof