seqf1olem2a

	Ref	Expression
Hypotheses	seqf1o.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqf1o.2	$⊢ (φ \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
	seqf1o.3	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	seqf1o.4	$⊢ φ \to N \in ℤ_{\geq M}$
	seqf1o.5	$⊢ φ \to C \subseteq S$
	seqf1olem2a.1	$⊢ φ \to G : A ⟶ C$
	seqf1olem2a.3	$⊢ φ \to K \in A$
	seqf1olem2a.4	$⊢ φ \to (M \dots N) \subseteq A$
Assertion	seqf1olem2a	$⊢ φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (N) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (K)$

Proof

Step	Hyp	Ref	Expression
1		seqf1o.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
2		seqf1o.2	$⊢ (φ \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
3		seqf1o.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		seqf1o.4	$⊢ φ \to N \in ℤ_{\geq M}$
5		seqf1o.5	$⊢ φ \to C \subseteq S$
6		seqf1olem2a.1	$⊢ φ \to G : A ⟶ C$
7		seqf1olem2a.3	$⊢ φ \to K \in A$
8		seqf1olem2a.4	$⊢ φ \to (M \dots N) \subseteq A$
9		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
10	4 9	syl	$⊢ φ \to N \in (M \dots N)$
11		fveq2	$⊢ m = M \to seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (M)$
12	11	oveq2d	$⊢ m = M \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (M)$
13	11	oveq1d	$⊢ m = M \to seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K) = seq M (\underset{˙}{+}, G) (M) \underset{˙}{+} G (K)$
14	12 13	eqeq12d	$⊢ m = M \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K) \leftrightarrow G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (M) = seq M (\underset{˙}{+}, G) (M) \underset{˙}{+} G (K))$
15	14	imbi2d	$⊢ m = M \to ((φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K)) \leftrightarrow (φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (M) = seq M (\underset{˙}{+}, G) (M) \underset{˙}{+} G (K)))$
16		fveq2	$⊢ m = n \to seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (n)$
17	16	oveq2d	$⊢ m = n \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n)$
18	16	oveq1d	$⊢ m = n \to seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K)$
19	17 18	eqeq12d	$⊢ m = n \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K) \leftrightarrow G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K))$
20	19	imbi2d	$⊢ m = n \to ((φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K)) \leftrightarrow (φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K)))$
21		fveq2	$⊢ m = n + 1 \to seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (n + 1)$
22	21	oveq2d	$⊢ m = n + 1 \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1)$
23	21	oveq1d	$⊢ m = n + 1 \to seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K) = seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K)$
24	22 23	eqeq12d	$⊢ m = n + 1 \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K) \leftrightarrow G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K))$
25	24	imbi2d	$⊢ m = n + 1 \to ((φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K)) \leftrightarrow (φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K)))$
26		fveq2	$⊢ m = N \to seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (N)$
27	26	oveq2d	$⊢ m = N \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (N)$
28	26	oveq1d	$⊢ m = N \to seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (K)$
29	27 28	eqeq12d	$⊢ m = N \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K) \leftrightarrow G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (N) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (K))$
30	29	imbi2d	$⊢ m = N \to ((φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (m) = seq M (\underset{˙}{+}, G) (m) \underset{˙}{+} G (K)) \leftrightarrow (φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (N) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (K)))$
31	6 7	ffvelcdmd	$⊢ φ \to G (K) \in C$
32		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
33		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, G) (M) = G (M)$
34	4 32 33	3syl	$⊢ φ \to seq M (\underset{˙}{+}, G) (M) = G (M)$
35		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
36	4 35	syl	$⊢ φ \to M \in (M \dots N)$
37	8 36	sseldd	$⊢ φ \to M \in A$
38	6 37	ffvelcdmd	$⊢ φ \to G (M) \in C$
39	34 38	eqeltrd	$⊢ φ \to seq M (\underset{˙}{+}, G) (M) \in C$
40	2 31 39	caovcomd	$⊢ φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (M) = seq M (\underset{˙}{+}, G) (M) \underset{˙}{+} G (K)$
41	40	a1i	$⊢ N \in ℤ_{\geq M} \to (φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (M) = seq M (\underset{˙}{+}, G) (M) \underset{˙}{+} G (K))$
42		oveq1	$⊢ G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K) \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} G (n + 1) = (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K)) \underset{˙}{+} G (n + 1)$
43		elfzouz	$⊢ n \in (M ..^N) \to n \in ℤ_{\geq M}$
44	43	adantl	$⊢ (φ \land n \in (M ..^N)) \to n \in ℤ_{\geq M}$
45		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)$
46	44 45	syl	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)$
47	46	oveq2d	$⊢ (φ \land n \in (M ..^N)) \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1) = G (K) \underset{˙}{+} (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1))$
48	3	adantlr	$⊢ ((φ \land n \in (M ..^N)) \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
49	5 31	sseldd	$⊢ φ \to G (K) \in S$
50	49	adantr	$⊢ (φ \land n \in (M ..^N)) \to G (K) \in S$
51	5	adantr	$⊢ (φ \land n \in (M ..^N)) \to C \subseteq S$
52	51	adantr	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots n)) \to C \subseteq S$
53	6	adantr	$⊢ (φ \land n \in (M ..^N)) \to G : A ⟶ C$
54	53	adantr	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots n)) \to G : A ⟶ C$
55		elfzouz2	$⊢ n \in (M ..^N) \to N \in ℤ_{\geq n}$
56	55	adantl	$⊢ (φ \land n \in (M ..^N)) \to N \in ℤ_{\geq n}$
57		fzss2	$⊢ N \in ℤ_{\geq n} \to (M \dots n) \subseteq (M \dots N)$
58	56 57	syl	$⊢ (φ \land n \in (M ..^N)) \to (M \dots n) \subseteq (M \dots N)$
59	8	adantr	$⊢ (φ \land n \in (M ..^N)) \to (M \dots N) \subseteq A$
60	58 59	sstrd	$⊢ (φ \land n \in (M ..^N)) \to (M \dots n) \subseteq A$
61	60	sselda	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots n)) \to x \in A$
62	54 61	ffvelcdmd	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots n)) \to G (x) \in C$
63	52 62	sseldd	$⊢ ((φ \land n \in (M ..^N)) \land x \in (M \dots n)) \to G (x) \in S$
64	1	adantlr	$⊢ ((φ \land n \in (M ..^N)) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
65	44 63 64	seqcl	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, G) (n) \in S$
66		fzofzp1	$⊢ n \in (M ..^N) \to n + 1 \in (M \dots N)$
67	66	adantl	$⊢ (φ \land n \in (M ..^N)) \to n + 1 \in (M \dots N)$
68	59 67	sseldd	$⊢ (φ \land n \in (M ..^N)) \to n + 1 \in A$
69	53 68	ffvelcdmd	$⊢ (φ \land n \in (M ..^N)) \to G (n + 1) \in C$
70	51 69	sseldd	$⊢ (φ \land n \in (M ..^N)) \to G (n + 1) \in S$
71	48 50 65 70	caovassd	$⊢ (φ \land n \in (M ..^N)) \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} G (n + 1) = G (K) \underset{˙}{+} (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1))$
72	47 71	eqtr4d	$⊢ (φ \land n \in (M ..^N)) \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1) = (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} G (n + 1)$
73	48 65 70 50	caovassd	$⊢ (φ \land n \in (M ..^N)) \to (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)) \underset{˙}{+} G (K) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} (G (n + 1) \underset{˙}{+} G (K))$
74	46	oveq1d	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K) = (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)) \underset{˙}{+} G (K)$
75	48 65 50 70	caovassd	$⊢ (φ \land n \in (M ..^N)) \to (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K)) \underset{˙}{+} G (n + 1) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} (G (K) \underset{˙}{+} G (n + 1))$
76	2	adantlr	$⊢ ((φ \land n \in (M ..^N)) \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
77	31	adantr	$⊢ (φ \land n \in (M ..^N)) \to G (K) \in C$
78	76 69 77	caovcomd	$⊢ (φ \land n \in (M ..^N)) \to G (n + 1) \underset{˙}{+} G (K) = G (K) \underset{˙}{+} G (n + 1)$
79	78	oveq2d	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} (G (n + 1) \underset{˙}{+} G (K)) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} (G (K) \underset{˙}{+} G (n + 1))$
80	75 79	eqtr4d	$⊢ (φ \land n \in (M ..^N)) \to (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K)) \underset{˙}{+} G (n + 1) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} (G (n + 1) \underset{˙}{+} G (K))$
81	73 74 80	3eqtr4d	$⊢ (φ \land n \in (M ..^N)) \to seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K) = (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K)) \underset{˙}{+} G (n + 1)$
82	72 81	eqeq12d	$⊢ (φ \land n \in (M ..^N)) \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K) \leftrightarrow (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n)) \underset{˙}{+} G (n + 1) = (seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K)) \underset{˙}{+} G (n + 1))$
83	42 82	imbitrrid	$⊢ (φ \land n \in (M ..^N)) \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K) \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K))$
84	83	expcom	$⊢ n \in (M ..^N) \to (φ \to (G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K) \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K)))$
85	84	a2d	$⊢ n \in (M ..^N) \to ((φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n) = seq M (\underset{˙}{+}, G) (n) \underset{˙}{+} G (K)) \to (φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (n + 1) = seq M (\underset{˙}{+}, G) (n + 1) \underset{˙}{+} G (K)))$
86	15 20 25 30 41 85	fzind2	$⊢ N \in (M \dots N) \to (φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (N) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (K))$
87	10 86	mpcom	$⊢ φ \to G (K) \underset{˙}{+} seq M (\underset{˙}{+}, G) (N) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (K)$

Metamath Proof Explorer

Theorem seqf1olem2a

Proof