seqcaopr2

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

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

Proof

Step	Hyp	Ref	Expression
1		seqcaopr2.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
2		seqcaopr2.2	$⊢ (φ \land (x \in S \land y \in S)) \to x Q y \in S$
3		seqcaopr2.3	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S))) \to (x Q z) \underset{˙}{+} (y Q w) = (x \underset{˙}{+} y) Q (z \underset{˙}{+} w)$
4		seqcaopr2.4	$⊢ φ \to N \in ℤ_{\geq M}$
5		seqcaopr2.5	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in S$
6		seqcaopr2.6	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in S$
7		seqcaopr2.7	$⊢ (φ \land k \in (M \dots N)) \to H (k) = F (k) Q G (k)$
8		elfzouz	$⊢ n \in (M ..^N) \to n \in ℤ_{\geq M}$
9	8	adantl	$⊢ (φ \land n \in (M ..^N)) \to n \in ℤ_{\geq M}$
10		elfzouz2	$⊢ n \in (M ..^N) \to N \in ℤ_{\geq n}$
11	10	adantl	$⊢ (φ \land n \in (M ..^N)) \to N \in ℤ_{\geq n}$
12		fzss2	$⊢ N \in ℤ_{\geq n} \to (M \dots n) \subseteq (M \dots N)$
13	11 12	syl	$⊢ (φ \land n \in (M ..^N)) \to (M \dots n) \subseteq (M \dots N)$
14	13	sselda	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots n)) \to x \in (M \dots N)$
15	6	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) G (k) \in S$
16	15	adantr	$⊢ (φ \land n \in (M ..^N)) \to \forall k \in (M \dots N) G (k) \in S$
17		fveq2	$⊢ k = x \to G (k) = G (x)$
18	17	eleq1d	$⊢ k = x \to (G (k) \in S \leftrightarrow G (x) \in S)$
19	18	rspccva	$⊢ (\forall k \in (M \dots N) G (k) \in S \land x \in (M \dots N)) \to G (x) \in S$
20	16 19	sylan	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots N)) \to G (x) \in S$
21	14 20	syldan	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots n)) \to G (x) \in S$
22	1	adantlr	$⊢ ((φ \land n \in (M ..^N)) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
23	9 21 22	seqcl	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, G) (n) \in S$
24		fzofzp1	$⊢ n \in (M ..^N) \to n + 1 \in (M \dots N)$
25		fveq2	$⊢ k = n + 1 \to G (k) = G (n + 1)$
26	25	eleq1d	$⊢ k = n + 1 \to (G (k) \in S \leftrightarrow G (n + 1) \in S)$
27	26	rspccva	$⊢ (\forall k \in (M \dots N) G (k) \in S \land n + 1 \in (M \dots N)) \to G (n + 1) \in S$
28	15 24 27	syl2an	$⊢ (φ \land n \in (M ..^N)) \to G (n + 1) \in S$
29	5	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) \in S$
30		fveq2	$⊢ k = x \to F (k) = F (x)$
31	30	eleq1d	$⊢ k = x \to (F (k) \in S \leftrightarrow F (x) \in S)$
32	31	rspccva	$⊢ (\forall k \in (M \dots N) F (k) \in S \land x \in (M \dots N)) \to F (x) \in S$
33	29 32	sylan	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
34	33	adantlr	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots N)) \to F (x) \in S$
35	14 34	syldan	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots n)) \to F (x) \in S$
36	9 35 22	seqcl	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, F) (n) \in S$
37		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
38	37	eleq1d	$⊢ k = n + 1 \to (F (k) \in S \leftrightarrow F (n + 1) \in S)$
39	38	rspccva	$⊢ (\forall k \in (M \dots N) F (k) \in S \land n + 1 \in (M \dots N)) \to F (n + 1) \in S$
40	29 24 39	syl2an	$⊢ (φ \land n \in (M ..^N)) \to F (n + 1) \in S$
41	3	anassrs	$⊢ ((φ \land (x \in S \land y \in S)) \land (z \in S \land w \in S)) \to (x Q z) \underset{˙}{+} (y Q w) = (x \underset{˙}{+} y) Q (z \underset{˙}{+} w)$
42	41	ralrimivva	$⊢ (φ \land (x \in S \land y \in S)) \to \forall z \in S \forall w \in S (x Q z) \underset{˙}{+} (y Q w) = (x \underset{˙}{+} y) Q (z \underset{˙}{+} w)$
43	42	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in S \forall z \in S \forall w \in S (x Q z) \underset{˙}{+} (y Q w) = (x \underset{˙}{+} y) Q (z \underset{˙}{+} w)$
44	43	adantr	$⊢ (φ \land n \in (M ..^N)) \to \forall x \in S \forall y \in S \forall z \in S \forall w \in S (x Q z) \underset{˙}{+} (y Q w) = (x \underset{˙}{+} y) Q (z \underset{˙}{+} w)$
45		oveq1	$⊢ x = seq M (\underset{˙}{+}, F) (n) \to x Q z = seq M (\underset{˙}{+}, F) (n) Q z$
46	45	oveq1d	$⊢ x = seq M (\underset{˙}{+}, F) (n) \to (x Q z) \underset{˙}{+} (y Q w) = (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (y Q w)$
47		oveq1	$⊢ x = seq M (\underset{˙}{+}, F) (n) \to x \underset{˙}{+} y = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} y$
48	47	oveq1d	$⊢ x = seq M (\underset{˙}{+}, F) (n) \to (x \underset{˙}{+} y) Q (z \underset{˙}{+} w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} y) Q (z \underset{˙}{+} w)$
49	46 48	eqeq12d	$⊢ x = seq M (\underset{˙}{+}, F) (n) \to ((x Q z) \underset{˙}{+} (y Q w) = (x \underset{˙}{+} y) Q (z \underset{˙}{+} w) \leftrightarrow (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (y Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} y) Q (z \underset{˙}{+} w))$
50	49	2ralbidv	$⊢ x = seq M (\underset{˙}{+}, F) (n) \to (\forall z \in S \forall w \in S (x Q z) \underset{˙}{+} (y Q w) = (x \underset{˙}{+} y) Q (z \underset{˙}{+} w) \leftrightarrow \forall z \in S \forall w \in S (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (y Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} y) Q (z \underset{˙}{+} w))$
51		oveq1	$⊢ y = F (n + 1) \to y Q w = F (n + 1) Q w$
52	51	oveq2d	$⊢ y = F (n + 1) \to (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (y Q w) = (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (F (n + 1) Q w)$
53		oveq2	$⊢ y = F (n + 1) \to seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} y = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
54	53	oveq1d	$⊢ y = F (n + 1) \to (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} y) Q (z \underset{˙}{+} w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (z \underset{˙}{+} w)$
55	52 54	eqeq12d	$⊢ y = F (n + 1) \to ((seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (y Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} y) Q (z \underset{˙}{+} w) \leftrightarrow (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (z \underset{˙}{+} w))$
56	55	2ralbidv	$⊢ y = F (n + 1) \to (\forall z \in S \forall w \in S (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (y Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} y) Q (z \underset{˙}{+} w) \leftrightarrow \forall z \in S \forall w \in S (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (z \underset{˙}{+} w))$
57	50 56	rspc2va	$⊢ ((seq M (\underset{˙}{+}, F) (n) \in S \land F (n + 1) \in S) \land \forall x \in S \forall y \in S \forall z \in S \forall w \in S (x Q z) \underset{˙}{+} (y Q w) = (x \underset{˙}{+} y) Q (z \underset{˙}{+} w)) \to \forall z \in S \forall w \in S (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (z \underset{˙}{+} w)$
58	36 40 44 57	syl21anc	$⊢ (φ \land n \in (M ..^N)) \to \forall z \in S \forall w \in S (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (z \underset{˙}{+} w)$
59		oveq2	$⊢ z = seq M (\underset{˙}{+}, G) (n) \to seq M (\underset{˙}{+}, F) (n) Q z = seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)$
60	59	oveq1d	$⊢ z = seq M (\underset{˙}{+}, G) (n) \to (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q w)$
61		oveq1	$⊢ z = seq M (\underset{˙}{+}, G) (n) \to z \underset{˙}{+} w = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} w$
62	61	oveq2d	$⊢ z = seq M (\underset{˙}{+}, G) (n) \to (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (z \underset{˙}{+} w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} w)$
63	60 62	eqeq12d	$⊢ z = seq M (\underset{˙}{+}, G) (n) \to ((seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (z \underset{˙}{+} w) \leftrightarrow (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} w))$
64		oveq2	$⊢ w = G (n + 1) \to F (n + 1) Q w = F (n + 1) Q G (n + 1)$
65	64	oveq2d	$⊢ w = G (n + 1) \to (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q G (n + 1))$
66		oveq2	$⊢ w = G (n + 1) \to seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} w = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)$
67	66	oveq2d	$⊢ w = G (n + 1) \to (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1))$
68	65 67	eqeq12d	$⊢ w = G (n + 1) \to ((seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} w) \leftrightarrow (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q G (n + 1)) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)))$
69	63 68	rspc2va	$⊢ ((seq M (\underset{˙}{+}, G) (n) \in S \land G (n + 1) \in S) \land \forall z \in S \forall w \in S (seq M (\underset{˙}{+}, F) (n) Q z) \underset{˙}{+} (F (n + 1) Q w) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (z \underset{˙}{+} w)) \to (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q G (n + 1)) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1))$
70	23 28 58 69	syl21anc	$⊢ (φ \land n \in (M ..^N)) \to (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q G (n + 1)) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1))$
71	1 2 4 5 6 7 70	seqcaopr3	$⊢ φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, F) (N) Q seq M (\underset{˙}{+}, G) (N)$

Metamath Proof Explorer

Theorem seqcaopr2

Proof