seqcaopr3

	Ref	Expression
Hypotheses	seqcaopr3.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqcaopr3.2	$⊢ (φ \land (x \in S \land y \in S)) \to x Q y \in S$
	seqcaopr3.3	$⊢ φ \to N \in ℤ_{\geq M}$
	seqcaopr3.4	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in S$
	seqcaopr3.5	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in S$
	seqcaopr3.6	$⊢ (φ \land k \in (M \dots N)) \to H (k) = F (k) Q G (k)$
	seqcaopr3.7	$⊢ (φ \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))$
Assertion	seqcaopr3	$⊢ φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, F) (N) Q seq M (\underset{˙}{+}, G) (N)$

Proof

Step	Hyp	Ref	Expression
1		seqcaopr3.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
2		seqcaopr3.2	$⊢ (φ \land (x \in S \land y \in S)) \to x Q y \in S$
3		seqcaopr3.3	$⊢ φ \to N \in ℤ_{\geq M}$
4		seqcaopr3.4	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in S$
5		seqcaopr3.5	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in S$
6		seqcaopr3.6	$⊢ (φ \land k \in (M \dots N)) \to H (k) = F (k) Q G (k)$
7		seqcaopr3.7	$⊢ (φ \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))$
8		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
9	3 8	syl	$⊢ φ \to N \in (M \dots N)$
10		fveq2	$⊢ z = M \to seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, H) (M)$
11		fveq2	$⊢ z = M \to seq M (\underset{˙}{+}, F) (z) = seq M (\underset{˙}{+}, F) (M)$
12		fveq2	$⊢ z = M \to seq M (\underset{˙}{+}, G) (z) = seq M (\underset{˙}{+}, G) (M)$
13	11 12	oveq12d	$⊢ z = M \to seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z) = seq M (\underset{˙}{+}, F) (M) Q seq M (\underset{˙}{+}, G) (M)$
14	10 13	eqeq12d	$⊢ z = M \to (seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z) \leftrightarrow seq M (\underset{˙}{+}, H) (M) = seq M (\underset{˙}{+}, F) (M) Q seq M (\underset{˙}{+}, G) (M))$
15	14	imbi2d	$⊢ z = M \to ((φ \to seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z)) \leftrightarrow (φ \to seq M (\underset{˙}{+}, H) (M) = seq M (\underset{˙}{+}, F) (M) Q seq M (\underset{˙}{+}, G) (M)))$
16		fveq2	$⊢ z = n \to seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, H) (n)$
17		fveq2	$⊢ z = n \to seq M (\underset{˙}{+}, F) (z) = seq M (\underset{˙}{+}, F) (n)$
18		fveq2	$⊢ z = n \to seq M (\underset{˙}{+}, G) (z) = seq M (\underset{˙}{+}, G) (n)$
19	17 18	oveq12d	$⊢ z = n \to seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z) = seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)$
20	16 19	eqeq12d	$⊢ z = n \to (seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z) \leftrightarrow seq M (\underset{˙}{+}, H) (n) = seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n))$
21	20	imbi2d	$⊢ z = n \to ((φ \to seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z)) \leftrightarrow (φ \to seq M (\underset{˙}{+}, H) (n) = seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)))$
22		fveq2	$⊢ z = n + 1 \to seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, H) (n + 1)$
23		fveq2	$⊢ z = n + 1 \to seq M (\underset{˙}{+}, F) (z) = seq M (\underset{˙}{+}, F) (n + 1)$
24		fveq2	$⊢ z = n + 1 \to seq M (\underset{˙}{+}, G) (z) = seq M (\underset{˙}{+}, G) (n + 1)$
25	23 24	oveq12d	$⊢ z = n + 1 \to seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z) = seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1)$
26	22 25	eqeq12d	$⊢ z = n + 1 \to (seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z) \leftrightarrow seq M (\underset{˙}{+}, H) (n + 1) = seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1))$
27	26	imbi2d	$⊢ z = n + 1 \to ((φ \to seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z)) \leftrightarrow (φ \to seq M (\underset{˙}{+}, H) (n + 1) = seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1)))$
28		fveq2	$⊢ z = N \to seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, H) (N)$
29		fveq2	$⊢ z = N \to seq M (\underset{˙}{+}, F) (z) = seq M (\underset{˙}{+}, F) (N)$
30		fveq2	$⊢ z = N \to seq M (\underset{˙}{+}, G) (z) = seq M (\underset{˙}{+}, G) (N)$
31	29 30	oveq12d	$⊢ z = N \to seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z) = seq M (\underset{˙}{+}, F) (N) Q seq M (\underset{˙}{+}, G) (N)$
32	28 31	eqeq12d	$⊢ z = N \to (seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z) \leftrightarrow seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, F) (N) Q seq M (\underset{˙}{+}, G) (N))$
33	32	imbi2d	$⊢ z = N \to ((φ \to seq M (\underset{˙}{+}, H) (z) = seq M (\underset{˙}{+}, F) (z) Q seq M (\underset{˙}{+}, G) (z)) \leftrightarrow (φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, F) (N) Q seq M (\underset{˙}{+}, G) (N)))$
34		fveq2	$⊢ k = M \to H (k) = H (M)$
35		fveq2	$⊢ k = M \to F (k) = F (M)$
36		fveq2	$⊢ k = M \to G (k) = G (M)$
37	35 36	oveq12d	$⊢ k = M \to F (k) Q G (k) = F (M) Q G (M)$
38	34 37	eqeq12d	$⊢ k = M \to (H (k) = F (k) Q G (k) \leftrightarrow H (M) = F (M) Q G (M))$
39	6	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) H (k) = F (k) Q G (k)$
40		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
41	3 40	syl	$⊢ φ \to M \in (M \dots N)$
42	38 39 41	rspcdva	$⊢ φ \to H (M) = F (M) Q G (M)$
43		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
44	3 43	syl	$⊢ φ \to M \in ℤ$
45		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, H) (M) = H (M)$
46	44 45	syl	$⊢ φ \to seq M (\underset{˙}{+}, H) (M) = H (M)$
47		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) (M) = F (M)$
48		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, G) (M) = G (M)$
49	47 48	oveq12d	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) (M) Q seq M (\underset{˙}{+}, G) (M) = F (M) Q G (M)$
50	44 49	syl	$⊢ φ \to seq M (\underset{˙}{+}, F) (M) Q seq M (\underset{˙}{+}, G) (M) = F (M) Q G (M)$
51	42 46 50	3eqtr4d	$⊢ φ \to seq M (\underset{˙}{+}, H) (M) = seq M (\underset{˙}{+}, F) (M) Q seq M (\underset{˙}{+}, G) (M)$
52	51	a1i	$⊢ N \in ℤ_{\geq M} \to (φ \to seq M (\underset{˙}{+}, H) (M) = seq M (\underset{˙}{+}, F) (M) Q seq M (\underset{˙}{+}, G) (M))$
53		oveq1	$⊢ seq M (\underset{˙}{+}, H) (n) = seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n) \to seq M (\underset{˙}{+}, H) (n) \underset{˙}{+} H (n + 1) = (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} H (n + 1)$
54		elfzouz	$⊢ n \in (M ..^N) \to n \in ℤ_{\geq M}$
55	54	adantl	$⊢ (φ \land n \in (M ..^N)) \to n \in ℤ_{\geq M}$
56		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, H) (n + 1) = seq M (\underset{˙}{+}, H) (n) \underset{˙}{+} H (n + 1)$
57	55 56	syl	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, H) (n + 1) = seq M (\underset{˙}{+}, H) (n) \underset{˙}{+} H (n + 1)$
58		fveq2	$⊢ k = n + 1 \to H (k) = H (n + 1)$
59		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
60		fveq2	$⊢ k = n + 1 \to G (k) = G (n + 1)$
61	59 60	oveq12d	$⊢ k = n + 1 \to F (k) Q G (k) = F (n + 1) Q G (n + 1)$
62	58 61	eqeq12d	$⊢ k = n + 1 \to (H (k) = F (k) Q G (k) \leftrightarrow H (n + 1) = F (n + 1) Q G (n + 1))$
63	39	adantr	$⊢ (φ \land n \in (M ..^N)) \to \forall k \in (M \dots N) H (k) = F (k) Q G (k)$
64		fzofzp1	$⊢ n \in (M ..^N) \to n + 1 \in (M \dots N)$
65	64	adantl	$⊢ (φ \land n \in (M ..^N)) \to n + 1 \in (M \dots N)$
66	62 63 65	rspcdva	$⊢ (φ \land n \in (M ..^N)) \to H (n + 1) = F (n + 1) Q G (n + 1)$
67	66	oveq2d	$⊢ (φ \land n \in (M ..^N)) \to (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} H (n + 1) = (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} (F (n + 1) Q G (n + 1))$
68		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, F) (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
69		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)$
70	68 69	oveq12d	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1))$
71	55 70	syl	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1) = (seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)) Q (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1))$
72	7 67 71	3eqtr4rd	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1) = (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} H (n + 1)$
73	57 72	eqeq12d	$⊢ (φ \land n \in (M ..^N)) \to (seq M (\underset{˙}{+}, H) (n + 1) = seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1) \leftrightarrow seq M (\underset{˙}{+}, H) (n) \underset{˙}{+} H (n + 1) = (seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} H (n + 1))$
74	53 73	imbitrrid	$⊢ (φ \land n \in (M ..^N)) \to (seq M (\underset{˙}{+}, H) (n) = seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n) \to seq M (\underset{˙}{+}, H) (n + 1) = seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1))$
75	74	expcom	$⊢ n \in (M ..^N) \to (φ \to (seq M (\underset{˙}{+}, H) (n) = seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n) \to seq M (\underset{˙}{+}, H) (n + 1) = seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1)))$
76	75	a2d	$⊢ n \in (M ..^N) \to ((φ \to seq M (\underset{˙}{+}, H) (n) = seq M (\underset{˙}{+}, F) (n) Q seq M (\underset{˙}{+}, G) (n)) \to (φ \to seq M (\underset{˙}{+}, H) (n + 1) = seq M (\underset{˙}{+}, F) (n + 1) Q seq M (\underset{˙}{+}, G) (n + 1)))$
77	15 21 27 33 52 76	fzind2	$⊢ N \in (M \dots N) \to (φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, F) (N) Q seq M (\underset{˙}{+}, G) (N))$
78	9 77	mpcom	$⊢ φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, F) (N) Q seq M (\underset{˙}{+}, G) (N)$

Metamath Proof Explorer

Theorem seqcaopr3

Proof