Metamath Proof Explorer


Theorem seqf1olem2

Description: Lemma for seqf1o . (Contributed by Mario Carneiro, 27-Feb-2014) (Revised by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses seqf1o.1 φ x S y S x + ˙ y S
seqf1o.2 φ x C y C x + ˙ y = y + ˙ x
seqf1o.3 φ x S y S z S x + ˙ y + ˙ z = x + ˙ y + ˙ z
seqf1o.4 φ N M
seqf1o.5 φ C S
seqf1olem.5 φ F : M N + 1 1-1 onto M N + 1
seqf1olem.6 φ G : M N + 1 C
seqf1olem.7 J = k M N F if k < K k k + 1
seqf1olem.8 K = F -1 N + 1
seqf1olem.9 φ g f f : M N 1-1 onto M N g : M N C seq M + ˙ g f N = seq M + ˙ g N
Assertion seqf1olem2 φ seq M + ˙ G F N + 1 = seq M + ˙ G N + 1

Proof

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