seqf1olem2

	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$
	seqf1olem.5	$⊢ φ \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
	seqf1olem.6	$⊢ φ \to G : (M \dots N + 1) ⟶ C$
	seqf1olem.7	$⊢ J = (k \in (M \dots N) ⟼ F (if (k < K, k, k + 1)))$
	seqf1olem.8	$⊢ K = F^{-1} (N + 1)$
	seqf1olem.9	$⊢ φ \to \forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N))$
Assertion	seqf1olem2	$⊢ φ \to seq M (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, G) (N + 1)$

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		seqf1olem.5	$⊢ φ \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
7		seqf1olem.6	$⊢ φ \to G : (M \dots N + 1) ⟶ C$
8		seqf1olem.7	$⊢ J = (k \in (M \dots N) ⟼ F (if (k < K, k, k + 1)))$
9		seqf1olem.8	$⊢ K = F^{-1} (N + 1)$
10		seqf1olem.9	$⊢ φ \to \forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N))$
11	7	ffnd	$⊢ φ \to G Fn (M \dots N + 1)$
12		fzssp1	$⊢ (M \dots N) \subseteq (M \dots N + 1)$
13		fnssres	$⊢ (G Fn (M \dots N + 1) \land (M \dots N) \subseteq (M \dots N + 1)) \to ({G ↾}_{(M \dots N)}) Fn (M \dots N)$
14	11 12 13	sylancl	$⊢ φ \to ({G ↾}_{(M \dots N)}) Fn (M \dots N)$
15		fzfid	$⊢ φ \to (M \dots N) \in Fin$
16		fnfi	$⊢ (({G ↾}_{(M \dots N)}) Fn (M \dots N) \land (M \dots N) \in Fin) \to {G ↾}_{(M \dots N)} \in Fin$
17	14 15 16	syl2anc	$⊢ φ \to {G ↾}_{(M \dots N)} \in Fin$
18	17	elexd	$⊢ φ \to {G ↾}_{(M \dots N)} \in V$
19	1 2 3 4 5 6 7 8 9	seqf1olem1	$⊢ φ \to J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N)$
20		f1of	$⊢ J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \to J : (M \dots N) ⟶ (M \dots N)$
21	19 20	syl	$⊢ φ \to J : (M \dots N) ⟶ (M \dots N)$
22		fex2	$⊢ (J : (M \dots N) ⟶ (M \dots N) \land (M \dots N) \in Fin \land (M \dots N) \in Fin) \to J \in V$
23	21 15 15 22	syl3anc	$⊢ φ \to J \in V$
24	18 23	jca	$⊢ φ \to ({G ↾}_{(M \dots N)} \in V \land J \in V)$
25		fssres	$⊢ (G : (M \dots N + 1) ⟶ C \land (M \dots N) \subseteq (M \dots N + 1)) \to ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ C$
26	7 12 25	sylancl	$⊢ φ \to ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ C$
27	19 26	jca	$⊢ φ \to (J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ C)$
28		f1oeq1	$⊢ f = J \to (f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \leftrightarrow J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N))$
29		feq1	$⊢ g = {G ↾}_{(M \dots N)} \to (g : (M \dots N) ⟶ C \leftrightarrow ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ C)$
30	28 29	bi2anan9r	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \leftrightarrow (J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ C))$
31		coeq1	$⊢ g = {G ↾}_{(M \dots N)} \to g \circ f = ({G ↾}_{(M \dots N)}) \circ f$
32		coeq2	$⊢ f = J \to ({G ↾}_{(M \dots N)}) \circ f = ({G ↾}_{(M \dots N)}) \circ J$
33	31 32	sylan9eq	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to g \circ f = ({G ↾}_{(M \dots N)}) \circ J$
34	33	seqeq3d	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to seq M (\underset{˙}{+}, (g \circ f)) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J))$
35	34	fveq1d	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)$
36		simpl	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to g = {G ↾}_{(M \dots N)}$
37	36	seqeq3d	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to seq M (\underset{˙}{+}, g) = seq M (\underset{˙}{+}, ({G ↾}_{(M \dots N)}))$
38	37	fveq1d	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to seq M (\underset{˙}{+}, g) (N) = seq M (\underset{˙}{+}, ({G ↾}_{(M \dots N)})) (N)$
39	35 38	eqeq12d	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to (seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N) \leftrightarrow seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, ({G ↾}_{(M \dots N)})) (N))$
40	30 39	imbi12d	$⊢ (g = {G ↾}_{(M \dots N)} \land f = J) \to (((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N)) \leftrightarrow ((J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, ({G ↾}_{(M \dots N)})) (N)))$
41	40	spc2gv	$⊢ ({G ↾}_{(M \dots N)} \in V \land J \in V) \to (\forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N)) \to ((J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, ({G ↾}_{(M \dots N)})) (N)))$
42	24 10 27 41	syl3c	$⊢ φ \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, ({G ↾}_{(M \dots N)})) (N)$
43		fvres	$⊢ x \in (M \dots N) \to ({G ↾}_{(M \dots N)}) (x) = G (x)$
44	43	adantl	$⊢ (φ \land x \in (M \dots N)) \to ({G ↾}_{(M \dots N)}) (x) = G (x)$
45	4 44	seqfveq	$⊢ φ \to seq M (\underset{˙}{+}, ({G ↾}_{(M \dots N)})) (N) = seq M (\underset{˙}{+}, G) (N)$
46	42 45	eqtrd	$⊢ φ \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, G) (N)$
47	46	oveq1d	$⊢ φ \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (N + 1)$
48	1	adantlr	$⊢ ((φ \land K \in (M \dots N)) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
49	3	adantlr	$⊢ ((φ \land K \in (M \dots N)) \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
50		elfzuz3	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq K}$
51	50	adantl	$⊢ (φ \land K \in (M \dots N)) \to N \in ℤ_{\geq K}$
52		eluzp1p1	$⊢ N \in ℤ_{\geq K} \to N + 1 \in ℤ_{\geq (K + 1)}$
53	51 52	syl	$⊢ (φ \land K \in (M \dots N)) \to N + 1 \in ℤ_{\geq (K + 1)}$
54		elfzuz	$⊢ K \in (M \dots N) \to K \in ℤ_{\geq M}$
55	54	adantl	$⊢ (φ \land K \in (M \dots N)) \to K \in ℤ_{\geq M}$
56		f1of	$⊢ F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \to F : (M \dots N + 1) ⟶ (M \dots N + 1)$
57	6 56	syl	$⊢ φ \to F : (M \dots N + 1) ⟶ (M \dots N + 1)$
58		fco	$⊢ (G : (M \dots N + 1) ⟶ C \land F : (M \dots N + 1) ⟶ (M \dots N + 1)) \to (G \circ F) : (M \dots N + 1) ⟶ C$
59	7 57 58	syl2anc	$⊢ φ \to (G \circ F) : (M \dots N + 1) ⟶ C$
60	59 5	fssd	$⊢ φ \to (G \circ F) : (M \dots N + 1) ⟶ S$
61	60	ffvelcdmda	$⊢ (φ \land x \in (M \dots N + 1)) \to (G \circ F) (x) \in S$
62	61	adantlr	$⊢ ((φ \land K \in (M \dots N)) \land x \in (M \dots N + 1)) \to (G \circ F) (x) \in S$
63	48 49 53 55 62	seqsplit	$⊢ (φ \land K \in (M \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (G \circ F)) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1)$
64		elfzp12	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow (K = M \lor K \in (M + 1 \dots N)))$
65	64	biimpa	$⊢ (N \in ℤ_{\geq M} \land K \in (M \dots N)) \to (K = M \lor K \in (M + 1 \dots N))$
66	4 65	sylan	$⊢ (φ \land K \in (M \dots N)) \to (K = M \lor K \in (M + 1 \dots N))$
67		seqeq1	$⊢ K = M \to seq K (\underset{˙}{+}, (G \circ F)) = seq M (\underset{˙}{+}, (G \circ F))$
68	67	eqcomd	$⊢ K = M \to seq M (\underset{˙}{+}, (G \circ F)) = seq K (\underset{˙}{+}, (G \circ F))$
69	68	fveq1d	$⊢ K = M \to seq M (\underset{˙}{+}, (G \circ F)) (K) = seq K (\underset{˙}{+}, (G \circ F)) (K)$
70		f1ocnv	$⊢ F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \to F^{-1} : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
71		f1of	$⊢ F^{-1} : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \to F^{-1} : (M \dots N + 1) ⟶ (M \dots N + 1)$
72	6 70 71	3syl	$⊢ φ \to F^{-1} : (M \dots N + 1) ⟶ (M \dots N + 1)$
73		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
74		eluzfz2	$⊢ N + 1 \in ℤ_{\geq M} \to N + 1 \in (M \dots N + 1)$
75	4 73 74	3syl	$⊢ φ \to N + 1 \in (M \dots N + 1)$
76	72 75	ffvelcdmd	$⊢ φ \to F^{-1} (N + 1) \in (M \dots N + 1)$
77	9 76	eqeltrid	$⊢ φ \to K \in (M \dots N + 1)$
78		elfzelz	$⊢ K \in (M \dots N + 1) \to K \in ℤ$
79		seq1	$⊢ K \in ℤ \to seq K (\underset{˙}{+}, (G \circ F)) (K) = (G \circ F) (K)$
80	77 78 79	3syl	$⊢ φ \to seq K (\underset{˙}{+}, (G \circ F)) (K) = (G \circ F) (K)$
81	69 80	sylan9eqr	$⊢ (φ \land K = M) \to seq M (\underset{˙}{+}, (G \circ F)) (K) = (G \circ F) (K)$
82	81	oveq1d	$⊢ (φ \land K = M) \to seq M (\underset{˙}{+}, (G \circ F)) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = (G \circ F) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1)$
83		simpr	$⊢ (φ \land K = M) \to K = M$
84		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
85	4 84	syl	$⊢ φ \to M \in (M \dots N)$
86	85	adantr	$⊢ (φ \land K = M) \to M \in (M \dots N)$
87	83 86	eqeltrd	$⊢ (φ \land K = M) \to K \in (M \dots N)$
88	2	adantlr	$⊢ ((φ \land K \in (M \dots N)) \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
89	5	adantr	$⊢ (φ \land K \in (M \dots N)) \to C \subseteq S$
90	59	adantr	$⊢ (φ \land K \in (M \dots N)) \to (G \circ F) : (M \dots N + 1) ⟶ C$
91	77	adantr	$⊢ (φ \land K \in (M \dots N)) \to K \in (M \dots N + 1)$
92		peano2uz	$⊢ K \in ℤ_{\geq M} \to K + 1 \in ℤ_{\geq M}$
93		fzss1	$⊢ K + 1 \in ℤ_{\geq M} \to (K + 1 \dots N + 1) \subseteq (M \dots N + 1)$
94	55 92 93	3syl	$⊢ (φ \land K \in (M \dots N)) \to (K + 1 \dots N + 1) \subseteq (M \dots N + 1)$
95	48 88 49 53 89 90 91 94	seqf1olem2a	$⊢ (φ \land K \in (M \dots N)) \to (G \circ F) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) \underset{˙}{+} (G \circ F) (K)$
96		1zzd	$⊢ (φ \land K \in (M \dots N)) \to 1 \in ℤ$
97		elfzuz	$⊢ K \in (M \dots N + 1) \to K \in ℤ_{\geq M}$
98		fzss1	$⊢ K \in ℤ_{\geq M} \to (K \dots N) \subseteq (M \dots N)$
99	77 97 98	3syl	$⊢ φ \to (K \dots N) \subseteq (M \dots N)$
100	99	sselda	$⊢ (φ \land x \in (K \dots N)) \to x \in (M \dots N)$
101	21	ffvelcdmda	$⊢ (φ \land x \in (M \dots N)) \to J (x) \in (M \dots N)$
102	100 101	syldan	$⊢ (φ \land x \in (K \dots N)) \to J (x) \in (M \dots N)$
103	102	fvresd	$⊢ (φ \land x \in (K \dots N)) \to ({G ↾}_{(M \dots N)}) (J (x)) = G (J (x))$
104		breq1	$⊢ k = x \to (k < K \leftrightarrow x < K)$
105		id	$⊢ k = x \to k = x$
106		oveq1	$⊢ k = x \to k + 1 = x + 1$
107	104 105 106	ifbieq12d	$⊢ k = x \to if (k < K, k, k + 1) = if (x < K, x, x + 1)$
108	107	fveq2d	$⊢ k = x \to F (if (k < K, k, k + 1)) = F (if (x < K, x, x + 1))$
109		fvex	$⊢ F (if (x < K, x, x + 1)) \in V$
110	108 8 109	fvmpt	$⊢ x \in (M \dots N) \to J (x) = F (if (x < K, x, x + 1))$
111	100 110	syl	$⊢ (φ \land x \in (K \dots N)) \to J (x) = F (if (x < K, x, x + 1))$
112	77 78	syl	$⊢ φ \to K \in ℤ$
113	112	zred	$⊢ φ \to K \in ℝ$
114	113	adantr	$⊢ (φ \land x \in (K \dots N)) \to K \in ℝ$
115		elfzelz	$⊢ x \in (K \dots N) \to x \in ℤ$
116	115	adantl	$⊢ (φ \land x \in (K \dots N)) \to x \in ℤ$
117	116	zred	$⊢ (φ \land x \in (K \dots N)) \to x \in ℝ$
118		elfzle1	$⊢ x \in (K \dots N) \to K \leq x$
119	118	adantl	$⊢ (φ \land x \in (K \dots N)) \to K \leq x$
120	114 117 119	lensymd	$⊢ (φ \land x \in (K \dots N)) \to \neg x < K$
121		iffalse	$⊢ \neg x < K \to if (x < K, x, x + 1) = x + 1$
122	121	fveq2d	$⊢ \neg x < K \to F (if (x < K, x, x + 1)) = F (x + 1)$
123	120 122	syl	$⊢ (φ \land x \in (K \dots N)) \to F (if (x < K, x, x + 1)) = F (x + 1)$
124	111 123	eqtrd	$⊢ (φ \land x \in (K \dots N)) \to J (x) = F (x + 1)$
125	124	fveq2d	$⊢ (φ \land x \in (K \dots N)) \to G (J (x)) = G (F (x + 1))$
126	103 125	eqtrd	$⊢ (φ \land x \in (K \dots N)) \to ({G ↾}_{(M \dots N)}) (J (x)) = G (F (x + 1))$
127		fvco3	$⊢ (J : (M \dots N) ⟶ (M \dots N) \land x \in (M \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) = ({G ↾}_{(M \dots N)}) (J (x))$
128	21 127	sylan	$⊢ (φ \land x \in (M \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) = ({G ↾}_{(M \dots N)}) (J (x))$
129	100 128	syldan	$⊢ (φ \land x \in (K \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) = ({G ↾}_{(M \dots N)}) (J (x))$
130		fzp1elp1	$⊢ x \in (M \dots N) \to x + 1 \in (M \dots N + 1)$
131	100 130	syl	$⊢ (φ \land x \in (K \dots N)) \to x + 1 \in (M \dots N + 1)$
132		fvco3	$⊢ (F : (M \dots N + 1) ⟶ (M \dots N + 1) \land x + 1 \in (M \dots N + 1)) \to (G \circ F) (x + 1) = G (F (x + 1))$
133	57 132	sylan	$⊢ (φ \land x + 1 \in (M \dots N + 1)) \to (G \circ F) (x + 1) = G (F (x + 1))$
134	131 133	syldan	$⊢ (φ \land x \in (K \dots N)) \to (G \circ F) (x + 1) = G (F (x + 1))$
135	126 129 134	3eqtr4d	$⊢ (φ \land x \in (K \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) = (G \circ F) (x + 1)$
136	135	adantlr	$⊢ ((φ \land K \in (M \dots N)) \land x \in (K \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) = (G \circ F) (x + 1)$
137	51 96 136	seqshft2	$⊢ (φ \land K \in (M \dots N)) \to seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1)$
138		fvco3	$⊢ (F : (M \dots N + 1) ⟶ (M \dots N + 1) \land K \in (M \dots N + 1)) \to (G \circ F) (K) = G (F (K))$
139	57 77 138	syl2anc	$⊢ φ \to (G \circ F) (K) = G (F (K))$
140	9	fveq2i	$⊢ F (K) = F (F^{-1} (N + 1))$
141		f1ocnvfv2	$⊢ (F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \land N + 1 \in (M \dots N + 1)) \to F (F^{-1} (N + 1)) = N + 1$
142	6 75 141	syl2anc	$⊢ φ \to F (F^{-1} (N + 1)) = N + 1$
143	140 142	eqtrid	$⊢ φ \to F (K) = N + 1$
144	143	fveq2d	$⊢ φ \to G (F (K)) = G (N + 1)$
145	139 144	eqtr2d	$⊢ φ \to G (N + 1) = (G \circ F) (K)$
146	145	adantr	$⊢ (φ \land K \in (M \dots N)) \to G (N + 1) = (G \circ F) (K)$
147	137 146	oveq12d	$⊢ (φ \land K \in (M \dots N)) \to seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1) = seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) \underset{˙}{+} (G \circ F) (K)$
148	95 147	eqtr4d	$⊢ (φ \land K \in (M \dots N)) \to (G \circ F) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
149	87 148	syldan	$⊢ (φ \land K = M) \to (G \circ F) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
150	83	seqeq1d	$⊢ (φ \land K = M) \to seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J))$
151	150	fveq1d	$⊢ (φ \land K = M) \to seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)$
152	151	oveq1d	$⊢ (φ \land K = M) \to seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
153	82 149 152	3eqtrd	$⊢ (φ \land K = M) \to seq M (\underset{˙}{+}, (G \circ F)) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
154		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
155	4 154	syl	$⊢ φ \to M \in ℤ$
156		elfzuz	$⊢ K \in (M + 1 \dots N) \to K \in ℤ_{\geq (M + 1)}$
157		eluzp1m1	$⊢ (M \in ℤ \land K \in ℤ_{\geq (M + 1)}) \to K - 1 \in ℤ_{\geq M}$
158	155 156 157	syl2an	$⊢ (φ \land K \in (M + 1 \dots N)) \to K - 1 \in ℤ_{\geq M}$
159		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
160	4 159	syl	$⊢ φ \to N \in ℤ$
161	160	zcnd	$⊢ φ \to N \in ℂ$
162		ax-1cn	$⊢ 1 \in ℂ$
163		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
164	161 162 163	sylancl	$⊢ φ \to N + 1 - 1 = N$
165		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
166	77 78 165	3syl	$⊢ φ \to K - 1 \in ℤ$
167		elfzuz3	$⊢ K \in (M \dots N + 1) \to N + 1 \in ℤ_{\geq K}$
168	77 167	syl	$⊢ φ \to N + 1 \in ℤ_{\geq K}$
169	112	zcnd	$⊢ φ \to K \in ℂ$
170		npcan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K - 1 + 1 = K$
171	169 162 170	sylancl	$⊢ φ \to K - 1 + 1 = K$
172	171	fveq2d	$⊢ φ \to ℤ_{\geq (K - 1 + 1)} = ℤ_{\geq K}$
173	168 172	eleqtrrd	$⊢ φ \to N + 1 \in ℤ_{\geq (K - 1 + 1)}$
174		eluzp1m1	$⊢ (K - 1 \in ℤ \land N + 1 \in ℤ_{\geq (K - 1 + 1)}) \to N + 1 - 1 \in ℤ_{\geq (K - 1)}$
175	166 173 174	syl2anc	$⊢ φ \to N + 1 - 1 \in ℤ_{\geq (K - 1)}$
176	164 175	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (K - 1)}$
177		fzss2	$⊢ N \in ℤ_{\geq (K - 1)} \to (M \dots K - 1) \subseteq (M \dots N)$
178	176 177	syl	$⊢ φ \to (M \dots K - 1) \subseteq (M \dots N)$
179	178	sselda	$⊢ (φ \land x \in (M \dots K - 1)) \to x \in (M \dots N)$
180	179 101	syldan	$⊢ (φ \land x \in (M \dots K - 1)) \to J (x) \in (M \dots N)$
181	180	fvresd	$⊢ (φ \land x \in (M \dots K - 1)) \to ({G ↾}_{(M \dots N)}) (J (x)) = G (J (x))$
182	179 110	syl	$⊢ (φ \land x \in (M \dots K - 1)) \to J (x) = F (if (x < K, x, x + 1))$
183		elfzm11	$⊢ (M \in ℤ \land K \in ℤ) \to (x \in (M \dots K - 1) \leftrightarrow (x \in ℤ \land M \leq x \land x < K))$
184	155 112 183	syl2anc	$⊢ φ \to (x \in (M \dots K - 1) \leftrightarrow (x \in ℤ \land M \leq x \land x < K))$
185	184	biimpa	$⊢ (φ \land x \in (M \dots K - 1)) \to (x \in ℤ \land M \leq x \land x < K)$
186	185	simp3d	$⊢ (φ \land x \in (M \dots K - 1)) \to x < K$
187		iftrue	$⊢ x < K \to if (x < K, x, x + 1) = x$
188	187	fveq2d	$⊢ x < K \to F (if (x < K, x, x + 1)) = F (x)$
189	186 188	syl	$⊢ (φ \land x \in (M \dots K - 1)) \to F (if (x < K, x, x + 1)) = F (x)$
190	182 189	eqtrd	$⊢ (φ \land x \in (M \dots K - 1)) \to J (x) = F (x)$
191	190	fveq2d	$⊢ (φ \land x \in (M \dots K - 1)) \to G (J (x)) = G (F (x))$
192	181 191	eqtr2d	$⊢ (φ \land x \in (M \dots K - 1)) \to G (F (x)) = ({G ↾}_{(M \dots N)}) (J (x))$
193		peano2uz	$⊢ N \in ℤ_{\geq (K - 1)} \to N + 1 \in ℤ_{\geq (K - 1)}$
194		fzss2	$⊢ N + 1 \in ℤ_{\geq (K - 1)} \to (M \dots K - 1) \subseteq (M \dots N + 1)$
195	176 193 194	3syl	$⊢ φ \to (M \dots K - 1) \subseteq (M \dots N + 1)$
196	195	sselda	$⊢ (φ \land x \in (M \dots K - 1)) \to x \in (M \dots N + 1)$
197		fvco3	$⊢ (F : (M \dots N + 1) ⟶ (M \dots N + 1) \land x \in (M \dots N + 1)) \to (G \circ F) (x) = G (F (x))$
198	57 197	sylan	$⊢ (φ \land x \in (M \dots N + 1)) \to (G \circ F) (x) = G (F (x))$
199	196 198	syldan	$⊢ (φ \land x \in (M \dots K - 1)) \to (G \circ F) (x) = G (F (x))$
200	179 128	syldan	$⊢ (φ \land x \in (M \dots K - 1)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) = ({G ↾}_{(M \dots N)}) (J (x))$
201	192 199 200	3eqtr4d	$⊢ (φ \land x \in (M \dots K - 1)) \to (G \circ F) (x) = (({G ↾}_{(M \dots N)}) \circ J) (x)$
202	201	adantlr	$⊢ ((φ \land K \in (M + 1 \dots N)) \land x \in (M \dots K - 1)) \to (G \circ F) (x) = (({G ↾}_{(M \dots N)}) \circ J) (x)$
203	158 202	seqfveq	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (K - 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1)$
204		fzp1ss	$⊢ M \in ℤ \to (M + 1 \dots N) \subseteq (M \dots N)$
205	4 154 204	3syl	$⊢ φ \to (M + 1 \dots N) \subseteq (M \dots N)$
206	205	sselda	$⊢ (φ \land K \in (M + 1 \dots N)) \to K \in (M \dots N)$
207	206 148	syldan	$⊢ (φ \land K \in (M + 1 \dots N)) \to (G \circ F) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
208	203 207	oveq12d	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} ((G \circ F) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1)) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} (seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1))$
209	196 61	syldan	$⊢ (φ \land x \in (M \dots K - 1)) \to (G \circ F) (x) \in S$
210	209	adantlr	$⊢ ((φ \land K \in (M + 1 \dots N)) \land x \in (M \dots K - 1)) \to (G \circ F) (x) \in S$
211	1	adantlr	$⊢ ((φ \land K \in (M + 1 \dots N)) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
212	158 210 211	seqcl	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \in S$
213	59 77	ffvelcdmd	$⊢ φ \to (G \circ F) (K) \in C$
214	5 213	sseldd	$⊢ φ \to (G \circ F) (K) \in S$
215	214	adantr	$⊢ (φ \land K \in (M + 1 \dots N)) \to (G \circ F) (K) \in S$
216	94	sselda	$⊢ ((φ \land K \in (M \dots N)) \land x \in (K + 1 \dots N + 1)) \to x \in (M \dots N + 1)$
217	216 62	syldan	$⊢ ((φ \land K \in (M \dots N)) \land x \in (K + 1 \dots N + 1)) \to (G \circ F) (x) \in S$
218	53 217 48	seqcl	$⊢ (φ \land K \in (M \dots N)) \to seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) \in S$
219	206 218	syldan	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) \in S$
220	212 215 219	3jca	$⊢ (φ \land K \in (M + 1 \dots N)) \to (seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \in S \land (G \circ F) (K) \in S \land seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) \in S)$
221	3	caovassg	$⊢ (φ \land (seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \in S \land (G \circ F) (K) \in S \land seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) \in S)) \to (seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} (G \circ F) (K)) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} ((G \circ F) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1))$
222	220 221	syldan	$⊢ (φ \land K \in (M + 1 \dots N)) \to (seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} (G \circ F) (K)) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} ((G \circ F) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1))$
223	7 5	fssd	$⊢ φ \to G : (M \dots N + 1) ⟶ S$
224		fssres	$⊢ (G : (M \dots N + 1) ⟶ S \land (M \dots N) \subseteq (M \dots N + 1)) \to ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ S$
225	223 12 224	sylancl	$⊢ φ \to ({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ S$
226		fco	$⊢ (({G ↾}_{(M \dots N)}) : (M \dots N) ⟶ S \land J : (M \dots N) ⟶ (M \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) : (M \dots N) ⟶ S$
227	225 21 226	syl2anc	$⊢ φ \to (({G ↾}_{(M \dots N)}) \circ J) : (M \dots N) ⟶ S$
228	227	ffvelcdmda	$⊢ (φ \land x \in (M \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) \in S$
229	179 228	syldan	$⊢ (φ \land x \in (M \dots K - 1)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) \in S$
230	229	adantlr	$⊢ ((φ \land K \in (M + 1 \dots N)) \land x \in (M \dots K - 1)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) \in S$
231	158 230 211	seqcl	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \in S$
232		elfzuz3	$⊢ K \in (M + 1 \dots N) \to N \in ℤ_{\geq K}$
233	232	adantl	$⊢ (φ \land K \in (M + 1 \dots N)) \to N \in ℤ_{\geq K}$
234	100 228	syldan	$⊢ (φ \land x \in (K \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) \in S$
235	234	adantlr	$⊢ ((φ \land K \in (M + 1 \dots N)) \land x \in (K \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) \in S$
236	233 235 211	seqcl	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \in S$
237	223 75	ffvelcdmd	$⊢ φ \to G (N + 1) \in S$
238	237	adantr	$⊢ (φ \land K \in (M + 1 \dots N)) \to G (N + 1) \in S$
239	231 236 238	3jca	$⊢ (φ \land K \in (M + 1 \dots N)) \to (seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \in S \land seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \in S \land G (N + 1) \in S)$
240	3	caovassg	$⊢ (φ \land (seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \in S \land seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \in S \land G (N + 1) \in S)) \to (seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)) \underset{˙}{+} G (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} (seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1))$
241	239 240	syldan	$⊢ (φ \land K \in (M + 1 \dots N)) \to (seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)) \underset{˙}{+} G (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} (seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1))$
242	208 222 241	3eqtr4d	$⊢ (φ \land K \in (M + 1 \dots N)) \to (seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} (G \circ F) (K)) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = (seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)) \underset{˙}{+} G (N + 1)$
243		seqm1	$⊢ (M \in ℤ \land K \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, (G \circ F)) (K) = seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} (G \circ F) (K)$
244	155 156 243	syl2an	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (K) = seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} (G \circ F) (K)$
245	244	oveq1d	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = (seq M (\underset{˙}{+}, (G \circ F)) (K - 1) \underset{˙}{+} (G \circ F) (K)) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1)$
246	3	adantlr	$⊢ ((φ \land K \in (M + 1 \dots N)) \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
247		elfzelz	$⊢ K \in (M + 1 \dots N) \to K \in ℤ$
248	247	adantl	$⊢ (φ \land K \in (M + 1 \dots N)) \to K \in ℤ$
249	248	zcnd	$⊢ (φ \land K \in (M + 1 \dots N)) \to K \in ℂ$
250	249 162 170	sylancl	$⊢ (φ \land K \in (M + 1 \dots N)) \to K - 1 + 1 = K$
251	250	fveq2d	$⊢ (φ \land K \in (M + 1 \dots N)) \to ℤ_{\geq (K - 1 + 1)} = ℤ_{\geq K}$
252	233 251	eleqtrrd	$⊢ (φ \land K \in (M + 1 \dots N)) \to N \in ℤ_{\geq (K - 1 + 1)}$
253	228	adantlr	$⊢ ((φ \land K \in (M + 1 \dots N)) \land x \in (M \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) \in S$
254	211 246 252 158 253	seqsplit	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} seq (K - 1 + 1) (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)$
255	250	seqeq1d	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq (K - 1 + 1) (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) = seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J))$
256	255	fveq1d	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq (K - 1 + 1) (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)$
257	256	oveq2d	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} seq (K - 1 + 1) (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)$
258	254 257	eqtrd	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)$
259	258	oveq1d	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1) = (seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (K - 1) \underset{˙}{+} seq K (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)) \underset{˙}{+} G (N + 1)$
260	242 245 259	3eqtr4d	$⊢ (φ \land K \in (M + 1 \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
261	153 260	jaodan	$⊢ (φ \land (K = M \lor K \in (M + 1 \dots N))) \to seq M (\underset{˙}{+}, (G \circ F)) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
262	66 261	syldan	$⊢ (φ \land K \in (M \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (K) \underset{˙}{+} seq (K + 1) (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
263	63 262	eqtrd	$⊢ (φ \land K \in (M \dots N)) \to seq M (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
264	4	adantr	$⊢ (φ \land K = N + 1) \to N \in ℤ_{\geq M}$
265		seqp1	$⊢ N \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (G \circ F)) (N) \underset{˙}{+} (G \circ F) (N + 1)$
266	264 265	syl	$⊢ (φ \land K = N + 1) \to seq M (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (G \circ F)) (N) \underset{˙}{+} (G \circ F) (N + 1)$
267	110	adantl	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to J (x) = F (if (x < K, x, x + 1))$
268		elfzelz	$⊢ x \in (M \dots N) \to x \in ℤ$
269	268	zred	$⊢ x \in (M \dots N) \to x \in ℝ$
270	269	adantl	$⊢ (φ \land x \in (M \dots N)) \to x \in ℝ$
271	160	zred	$⊢ φ \to N \in ℝ$
272	271	adantr	$⊢ (φ \land x \in (M \dots N)) \to N \in ℝ$
273		peano2re	$⊢ N \in ℝ \to N + 1 \in ℝ$
274	272 273	syl	$⊢ (φ \land x \in (M \dots N)) \to N + 1 \in ℝ$
275		elfzle2	$⊢ x \in (M \dots N) \to x \leq N$
276	275	adantl	$⊢ (φ \land x \in (M \dots N)) \to x \leq N$
277	272	ltp1d	$⊢ (φ \land x \in (M \dots N)) \to N < N + 1$
278	270 272 274 276 277	lelttrd	$⊢ (φ \land x \in (M \dots N)) \to x < N + 1$
279	278	adantlr	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to x < N + 1$
280		simplr	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to K = N + 1$
281	279 280	breqtrrd	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to x < K$
282	281 188	syl	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to F (if (x < K, x, x + 1)) = F (x)$
283	267 282	eqtrd	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to J (x) = F (x)$
284	283	fveq2d	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to ({G ↾}_{(M \dots N)}) (J (x)) = ({G ↾}_{(M \dots N)}) (F (x))$
285	269	adantl	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to x \in ℝ$
286	285 281	gtned	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to K \neq x$
287	57	ad2antrr	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to F : (M \dots N + 1) ⟶ (M \dots N + 1)$
288		fzelp1	$⊢ x \in (M \dots N) \to x \in (M \dots N + 1)$
289	288	adantl	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to x \in (M \dots N + 1)$
290	287 289	ffvelcdmd	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to F (x) \in (M \dots N + 1)$
291	4	ad2antrr	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to N \in ℤ_{\geq M}$
292		elfzp1	$⊢ N \in ℤ_{\geq M} \to (F (x) \in (M \dots N + 1) \leftrightarrow (F (x) \in (M \dots N) \lor F (x) = N + 1))$
293	291 292	syl	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (F (x) \in (M \dots N + 1) \leftrightarrow (F (x) \in (M \dots N) \lor F (x) = N + 1))$
294	290 293	mpbid	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (F (x) \in (M \dots N) \lor F (x) = N + 1)$
295	294	ord	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (\neg F (x) \in (M \dots N) \to F (x) = N + 1)$
296	6	ad2antrr	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
297		f1ocnvfv	$⊢ (F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \land x \in (M \dots N + 1)) \to (F (x) = N + 1 \to F^{-1} (N + 1) = x)$
298	296 289 297	syl2anc	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (F (x) = N + 1 \to F^{-1} (N + 1) = x)$
299	9	eqeq1i	$⊢ K = x \leftrightarrow F^{-1} (N + 1) = x$
300	298 299	imbitrrdi	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (F (x) = N + 1 \to K = x)$
301	295 300	syld	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (\neg F (x) \in (M \dots N) \to K = x)$
302	301	necon1ad	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (K \neq x \to F (x) \in (M \dots N))$
303	286 302	mpd	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to F (x) \in (M \dots N)$
304	303	fvresd	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to ({G ↾}_{(M \dots N)}) (F (x)) = G (F (x))$
305	284 304	eqtr2d	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to G (F (x)) = ({G ↾}_{(M \dots N)}) (J (x))$
306	57 288 197	syl2an	$⊢ (φ \land x \in (M \dots N)) \to (G \circ F) (x) = G (F (x))$
307	306	adantlr	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (G \circ F) (x) = G (F (x))$
308	128	adantlr	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (({G ↾}_{(M \dots N)}) \circ J) (x) = ({G ↾}_{(M \dots N)}) (J (x))$
309	305 307 308	3eqtr4d	$⊢ ((φ \land K = N + 1) \land x \in (M \dots N)) \to (G \circ F) (x) = (({G ↾}_{(M \dots N)}) \circ J) (x)$
310	264 309	seqfveq	$⊢ (φ \land K = N + 1) \to seq M (\underset{˙}{+}, (G \circ F)) (N) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N)$
311		fvco3	$⊢ (F : (M \dots N + 1) ⟶ (M \dots N + 1) \land N + 1 \in (M \dots N + 1)) \to (G \circ F) (N + 1) = G (F (N + 1))$
312	57 75 311	syl2anc	$⊢ φ \to (G \circ F) (N + 1) = G (F (N + 1))$
313	312	adantr	$⊢ (φ \land K = N + 1) \to (G \circ F) (N + 1) = G (F (N + 1))$
314		simpr	$⊢ (φ \land K = N + 1) \to K = N + 1$
315	9 314	eqtr3id	$⊢ (φ \land K = N + 1) \to F^{-1} (N + 1) = N + 1$
316	315	fveq2d	$⊢ (φ \land K = N + 1) \to F (F^{-1} (N + 1)) = F (N + 1)$
317	142	adantr	$⊢ (φ \land K = N + 1) \to F (F^{-1} (N + 1)) = N + 1$
318	316 317	eqtr3d	$⊢ (φ \land K = N + 1) \to F (N + 1) = N + 1$
319	318	fveq2d	$⊢ (φ \land K = N + 1) \to G (F (N + 1)) = G (N + 1)$
320	313 319	eqtrd	$⊢ (φ \land K = N + 1) \to (G \circ F) (N + 1) = G (N + 1)$
321	310 320	oveq12d	$⊢ (φ \land K = N + 1) \to seq M (\underset{˙}{+}, (G \circ F)) (N) \underset{˙}{+} (G \circ F) (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
322	266 321	eqtrd	$⊢ (φ \land K = N + 1) \to seq M (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
323		elfzp1	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N + 1) \leftrightarrow (K \in (M \dots N) \lor K = N + 1))$
324	4 323	syl	$⊢ φ \to (K \in (M \dots N + 1) \leftrightarrow (K \in (M \dots N) \lor K = N + 1))$
325	77 324	mpbid	$⊢ φ \to (K \in (M \dots N) \lor K = N + 1)$
326	263 322 325	mpjaodan	$⊢ φ \to seq M (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, (({G ↾}_{(M \dots N)}) \circ J)) (N) \underset{˙}{+} G (N + 1)$
327		seqp1	$⊢ N \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, G) (N + 1) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (N + 1)$
328	4 327	syl	$⊢ φ \to seq M (\underset{˙}{+}, G) (N + 1) = seq M (\underset{˙}{+}, G) (N) \underset{˙}{+} G (N + 1)$
329	47 326 328	3eqtr4d	$⊢ φ \to seq M (\underset{˙}{+}, (G \circ F)) (N + 1) = seq M (\underset{˙}{+}, G) (N + 1)$

Metamath Proof Explorer

Theorem seqf1olem2

Proof