Theorem seqf1oglem2 10783

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

Hypotheses

Ref	Expression
seqf1o.1	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqf1o.2	|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
seqf1o.3	|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
seqf1o.4	|- ( ph -> N e. ( ZZ>= ` M ) )
seqf1o.5	|- ( ph -> C C_ S )
seqf1og.p	|- ( ph -> .+ e. V )
seqf1olem.5	|- ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
seqf1olem.6	|- ( ph -> G : ( M ... ( N + 1 ) ) --> C )
seqf1olem.7	|- J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
seqf1olem.8	|- K = ( `' F ` ( N + 1 ) )
seqf1olem.9	|- ( ph -> A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) )

Assertion

Ref	Expression
seqf1oglem2	|- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( seq M ( .+ , G ) ` ( N + 1 ) ) )

Distinct variable groups:   f, g, k, x, y, z, F   f, G, g, k, x, y, z   f, M, g, k, x, y, z   .+ , f, g, k, x, y, z   f, J, g, x, y, z   f, N, g, k, x, y, z   k, K, x, y, z   ph, f, g, k, x, y, z   S, k, x, y, z   C, f, g, k, x, y, z

Allowed substitution hints:   S( f, g)   J( k)   K( f, g)   V( x, y, z, f, g, k)

Proof of Theorem seqf1oglem2

Step	Hyp	Ref	Expression
1		seqf1olem.6	. . . . . . . . . 10 |- ( ph -> G : ( M ... ( N + 1 ) ) --> C )
2	1	ffnd 5483	. . . . . . . . 9 |- ( ph -> G Fn ( M ... ( N + 1 ) ) )
3		fzssp1 10302	. . . . . . . . 9 |- ( M ... N ) C_ ( M ... ( N + 1 ) )
4		fnssres 5445	. . . . . . . . 9 |- ( ( G Fn ( M ... ( N + 1 ) ) /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) Fn ( M ... N ) )
5	2, 3, 4	sylancl 413	. . . . . . . 8 |- ( ph -> ( G |` ( M ... N ) ) Fn ( M ... N ) )
6		seqf1o.4	. . . . . . . . . 10 |- ( ph -> N e. ( ZZ>= ` M ) )
7		eluzel2 9760	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
8	6, 7	syl 14	. . . . . . . . 9 |- ( ph -> M e. ZZ )
9		eluzelz 9765	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
10	6, 9	syl 14	. . . . . . . . 9 |- ( ph -> N e. ZZ )
11	8, 10	fzfigd 10694	. . . . . . . 8 |- ( ph -> ( M ... N ) e. Fin )
12		fnfi 7135	. . . . . . . 8 |- ( ( ( G |` ( M ... N ) ) Fn ( M ... N ) /\ ( M ... N ) e. Fin ) -> ( G |` ( M ... N ) ) e. Fin )
13	5, 11, 12	syl2anc 411	. . . . . . 7 |- ( ph -> ( G |` ( M ... N ) ) e. Fin )
14	13	elexd 2816	. . . . . 6 |- ( ph -> ( G |` ( M ... N ) ) e. _V )
15		seqf1o.1	. . . . . . . . 9 |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
16		seqf1o.2	. . . . . . . . 9 |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
17		seqf1o.3	. . . . . . . . 9 |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
18		seqf1o.5	. . . . . . . . 9 |- ( ph -> C C_ S )
19		seqf1og.p	. . . . . . . . 9 |- ( ph -> .+ e. V )
20		seqf1olem.5	. . . . . . . . 9 |- ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
21		seqf1olem.7	. . . . . . . . 9 |- J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
22		seqf1olem.8	. . . . . . . . 9 |- K = ( `' F ` ( N + 1 ) )
23	15, 16, 17, 6, 18, 19, 20, 1, 21, 22	seqf1oglem1 10782	. . . . . . . 8 |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
24		f1of 5583	. . . . . . . 8 |- ( J : ( M ... N ) -1-1-onto-> ( M ... N ) -> J : ( M ... N ) --> ( M ... N ) )
25	23, 24	syl 14	. . . . . . 7 |- ( ph -> J : ( M ... N ) --> ( M ... N ) )
26	25, 11	fexd 5884	. . . . . 6 |- ( ph -> J e. _V )
27	14, 26	jca 306	. . . . 5 |- ( ph -> ( ( G |` ( M ... N ) ) e. _V /\ J e. _V ) )
28		seqf1olem.9	. . . . 5 |- ( ph -> A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) )
29		fssres 5512	. . . . . . 7 |- ( ( G : ( M ... ( N + 1 ) ) --> C /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) : ( M ... N ) --> C )
30	1, 3, 29	sylancl 413	. . . . . 6 |- ( ph -> ( G |` ( M ... N ) ) : ( M ... N ) --> C )
31	23, 30	jca 306	. . . . 5 |- ( ph -> ( J : ( M ... N ) -1-1-onto-> ( M ... N ) /\ ( G |` ( M ... N ) ) : ( M ... N ) --> C ) )
32		f1oeq1 5571	. . . . . . . 8 |- ( f = J -> ( f : ( M ... N ) -1-1-onto-> ( M ... N ) <-> J : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
33		feq1 5465	. . . . . . . 8 |- ( g = ( G |` ( M ... N ) ) -> ( g : ( M ... N ) --> C <-> ( G |` ( M ... N ) ) : ( M ... N ) --> C ) )
34	32, 33	bi2anan9r 611	. . . . . . 7 |- ( ( 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 ) ) )
35		coeq1 4887	. . . . . . . . . . 11 |- ( g = ( G |` ( M ... N ) ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. f ) )
36		coeq2 4888	. . . . . . . . . . 11 |- ( f = J -> ( ( G |` ( M ... N ) ) o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
37	35, 36	sylan9eq 2284	. . . . . . . . . 10 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
38	37	seqeq3d 10718	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , ( g o. f ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
39	38	fveq1d 5641	. . . . . . . 8 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
40		simpl 109	. . . . . . . . . 10 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> g = ( G |` ( M ... N ) ) )
41	40	seqeq3d 10718	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , g ) = seq M ( .+ , ( G |` ( M ... N ) ) ) )
42	41	fveq1d 5641	. . . . . . . 8 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , g ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
43	39, 42	eqeq12d 2246	. . . . . . 7 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) <-> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) ) )
44	34, 43	imbi12d 234	. . . . . 6 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. 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 ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) ) ) )
45	44	spc2gv 2897	. . . . 5 |- ( ( ( G |` ( M ... N ) ) e. _V /\ J e. _V ) -> ( A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. 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 ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) ) ) )
46	27, 28, 31, 45	syl3c 63	. . . 4 |- ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
47		fvres 5663	. . . . . 6 |- ( x e. ( M ... N ) -> ( ( G |` ( M ... N ) ) ` x ) = ( G ` x ) )
48	47	adantl 277	. . . . 5 |- ( ( ph /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` x ) = ( G ` x ) )
49	10	peano2zd 9605	. . . . . . . 8 |- ( ph -> ( N + 1 ) e. ZZ )
50	8, 49	fzfigd 10694	. . . . . . 7 |- ( ph -> ( M ... ( N + 1 ) ) e. Fin )
51	1, 50	fexd 5884	. . . . . 6 |- ( ph -> G e. _V )
52		resexg 5053	. . . . . 6 |- ( G e. _V -> ( G |` ( M ... N ) ) e. _V )
53	51, 52	syl 14	. . . . 5 |- ( ph -> ( G |` ( M ... N ) ) e. _V )
54	6, 48, 19, 53, 51	seqfveqg 10741	. . . 4 |- ( ph -> ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
55	46, 54	eqtrd 2264	. . 3 |- ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
56	55	oveq1d 6033	. 2 |- ( ph -> ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
57	15	adantlr 477	. . . . 5 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
58	17	adantlr 477	. . . . 5 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
59		elfzuz3 10257	. . . . . . 7 |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
60	59	adantl 277	. . . . . 6 |- ( ( ph /\ K e. ( M ... N ) ) -> N e. ( ZZ>= ` K ) )
61		eluzp1p1 9782	. . . . . 6 |- ( N e. ( ZZ>= ` K ) -> ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
62	60, 61	syl 14	. . . . 5 |- ( ( ph /\ K e. ( M ... N ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
63	19	adantr 276	. . . . 5 |- ( ( ph /\ K e. ( M ... N ) ) -> .+ e. V )
64	51	adantr 276	. . . . . 6 |- ( ( ph /\ K e. ( M ... N ) ) -> G e. _V )
65		f1of 5583	. . . . . . . . 9 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
66	20, 65	syl 14	. . . . . . . 8 |- ( ph -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
67	66, 50	fexd 5884	. . . . . . 7 |- ( ph -> F e. _V )
68	67	adantr 276	. . . . . 6 |- ( ( ph /\ K e. ( M ... N ) ) -> F e. _V )
69		coexg 5281	. . . . . 6 |- ( ( G e. _V /\ F e. _V ) -> ( G o. F ) e. _V )
70	64, 68, 69	syl2anc 411	. . . . 5 |- ( ( ph /\ K e. ( M ... N ) ) -> ( G o. F ) e. _V )
71		elfzuz 10256	. . . . . 6 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
72	71	adantl 277	. . . . 5 |- ( ( ph /\ K e. ( M ... N ) ) -> K e. ( ZZ>= ` M ) )
73		fco 5500	. . . . . . . . 9 |- ( ( G : ( M ... ( N + 1 ) ) --> C /\ F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) ) -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
74	1, 66, 73	syl2anc 411	. . . . . . . 8 |- ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
75	74, 18	fssd 5495	. . . . . . 7 |- ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> S )
76	75	ffvelcdmda 5782	. . . . . 6 |- ( ( ph /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
77	76	adantlr 477	. . . . 5 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
78	57, 58, 62, 63, 70, 72, 77	seqsplitg 10752	. . . 4 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) )
79		elfzp12 10334	. . . . . . 7 |- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )
80	79	biimpa 296	. . . . . 6 |- ( ( N e. ( ZZ>= ` M ) /\ K e. ( M ... N ) ) -> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) )
81	6, 80	sylan 283	. . . . 5 |- ( ( ph /\ K e. ( M ... N ) ) -> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) )
82		seqeq1 10713	. . . . . . . . . . 11 |- ( K = M -> seq K ( .+ , ( G o. F ) ) = seq M ( .+ , ( G o. F ) ) )
83	82	eqcomd 2237	. . . . . . . . . 10 |- ( K = M -> seq M ( .+ , ( G o. F ) ) = seq K ( .+ , ( G o. F ) ) )
84	83	fveq1d 5641	. . . . . . . . 9 |- ( K = M -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( seq K ( .+ , ( G o. F ) ) ` K ) )
85		f1ocnv 5596	. . . . . . . . . . . . . 14 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
86		f1of 5583	. . . . . . . . . . . . . 14 |- ( `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
87	20, 85, 86	3syl 17	. . . . . . . . . . . . 13 |- ( ph -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
88		peano2uz 9817	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
89		eluzfz2 10267	. . . . . . . . . . . . . 14 |- ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
90	6, 88, 89	3syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
91	87, 90	ffvelcdmd 5783	. . . . . . . . . . . 12 |- ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
92	22, 91	eqeltrid 2318	. . . . . . . . . . 11 |- ( ph -> K e. ( M ... ( N + 1 ) ) )
93	92	elfzelzd 10261	. . . . . . . . . 10 |- ( ph -> K e. ZZ )
94	51, 67, 69	syl2anc 411	. . . . . . . . . 10 |- ( ph -> ( G o. F ) e. _V )
95		seq1g 10726	. . . . . . . . . 10 |- ( ( K e. ZZ /\ ( G o. F ) e. _V /\ .+ e. V ) -> ( seq K ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
96	93, 94, 19, 95	syl3anc 1273	. . . . . . . . 9 |- ( ph -> ( seq K ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
97	84, 96	sylan9eqr 2286	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
98	97	oveq1d 6033	. . . . . . 7 |- ( ( ph /\ K = M ) -> ( ( seq M ( .+ , ( G o. F ) ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( ( G o. F ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) )
99		simpr 110	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> K = M )
100		eluzfz1 10266	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
101	6, 100	syl 14	. . . . . . . . . 10 |- ( ph -> M e. ( M ... N ) )
102	101	adantr 276	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> M e. ( M ... N ) )
103	99, 102	eqeltrd 2308	. . . . . . . 8 |- ( ( ph /\ K = M ) -> K e. ( M ... N ) )
104	16	adantlr 477	. . . . . . . . . 10 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
105	18	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> C C_ S )
106	74	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
107	92	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> K e. ( M ... ( N + 1 ) ) )
108		peano2uz 9817	. . . . . . . . . . 11 |- ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
109		fzss1 10298	. . . . . . . . . . 11 |- ( ( K + 1 ) e. ( ZZ>= ` M ) -> ( ( K + 1 ) ... ( N + 1 ) ) C_ ( M ... ( N + 1 ) ) )
110	72, 108, 109	3syl 17	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( ( K + 1 ) ... ( N + 1 ) ) C_ ( M ... ( N + 1 ) ) )
111	50	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( M ... ( N + 1 ) ) e. Fin )
112	57, 104, 58, 62, 105, 63, 106, 107, 110, 111	seqf1oglem2a 10781	. . . . . . . . 9 |- ( ( ph /\ K e. ( M ... N ) ) -> ( ( ( G o. F ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) .+ ( ( G o. F ) ` K ) ) )
113		1zzd 9506	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( M ... N ) ) -> 1 e. ZZ )
114		elfzuz 10256	. . . . . . . . . . . . . . . . . 18 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ( ZZ>= ` M ) )
115		fzss1 10298	. . . . . . . . . . . . . . . . . 18 |- ( K e. ( ZZ>= ` M ) -> ( K ... N ) C_ ( M ... N ) )
116	92, 114, 115	3syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( K ... N ) C_ ( M ... N ) )
117	116	sselda 3227	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... N ) )
118	25	ffvelcdmda 5782	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( M ... N ) ) -> ( J ` x ) e. ( M ... N ) )
119	117, 118	syldan 282	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) e. ( M ... N ) )
120	119	fvresd 5664	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
121		breq1 4091	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> ( k < K <-> x < K ) )
122		id 19	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> k = x )
123		oveq1 6025	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> ( k + 1 ) = ( x + 1 ) )
124	121, 122, 123	ifbieq12d 3632	. . . . . . . . . . . . . . . . . 18 |- ( k = x -> if ( k < K , k , ( k + 1 ) ) = if ( x < K , x , ( x + 1 ) ) )
125	124	fveq2d 5643	. . . . . . . . . . . . . . . . 17 |- ( k = x -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
126	66	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
127	3, 117	sselid 3225	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... ( N + 1 ) ) )
128		fzp1elp1 10310	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( M ... N ) -> ( x + 1 ) e. ( M ... ( N + 1 ) ) )
129	117, 128	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> ( x + 1 ) e. ( M ... ( N + 1 ) ) )
130	117	elfzelzd 10261	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
131	93	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. ZZ )
132		zdclt 9557	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x e. ZZ /\ K e. ZZ ) -> DECID x < K )
133	130, 131, 132	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> DECID x < K )
134	127, 129, 133	ifcldcd 3643	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> if ( x < K , x , ( x + 1 ) ) e. ( M ... ( N + 1 ) ) )
135	126, 134	ffvelcdmd 5783	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) e. ( M ... ( N + 1 ) ) )
136	21, 125, 117, 135	fvmptd3 5740	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
137	93	zred 9602	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. RR )
138	137	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. RR )
139		elfzelz 10260	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( K ... N ) -> x e. ZZ )
140	139	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
141	140	zred 9602	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. RR )
142		elfzle1 10262	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( K ... N ) -> K <_ x )
143	142	adantl 277	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K <_ x )
144	138, 141, 143	lensymd 8301	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> -. x < K )
145		iffalse 3613	. . . . . . . . . . . . . . . . . 18 |- ( -. x < K -> if ( x < K , x , ( x + 1 ) ) = ( x + 1 ) )
146	145	fveq2d 5643	. . . . . . . . . . . . . . . . 17 |- ( -. x < K -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` ( x + 1 ) ) )
147	144, 146	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` ( x + 1 ) ) )
148	136, 147	eqtrd 2264	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` ( x + 1 ) ) )
149	148	fveq2d 5643	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
150	120, 149	eqtrd 2264	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
151		fvco3 5717	. . . . . . . . . . . . . . 15 |- ( ( J : ( M ... N ) --> ( M ... N ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
152	25, 151	sylan 283	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
153	117, 152	syldan 282	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
154		fvco3 5717	. . . . . . . . . . . . . . 15 |- ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ ( x + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
155	66, 154	sylan 283	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
156	129, 155	syldan 282	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
157	150, 153, 156	3eqtr4d 2274	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G o. F ) ` ( x + 1 ) ) )
158	157	adantlr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G o. F ) ` ( x + 1 ) ) )
159	64, 52	syl 14	. . . . . . . . . . . 12 |- ( ( ph /\ K e. ( M ... N ) ) -> ( G |` ( M ... N ) ) e. _V )
160	26	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ K e. ( M ... N ) ) -> J e. _V )
161		coexg 5281	. . . . . . . . . . . 12 |- ( ( ( G |` ( M ... N ) ) e. _V /\ J e. _V ) -> ( ( G |` ( M ... N ) ) o. J ) e. _V )
162	159, 160, 161	syl2anc 411	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) o. J ) e. _V )
163	60, 113, 158, 63, 162, 70	seqshft2g 10745	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) )
164		fvco3 5717	. . . . . . . . . . . . 13 |- ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ K e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` K ) = ( G ` ( F ` K ) ) )
165	66, 92, 164	syl2anc 411	. . . . . . . . . . . 12 |- ( ph -> ( ( G o. F ) ` K ) = ( G ` ( F ` K ) ) )
166	22	fveq2i 5642	. . . . . . . . . . . . . 14 |- ( F ` K ) = ( F ` ( `' F ` ( N + 1 ) ) )
167		f1ocnvfv2 5919	. . . . . . . . . . . . . . 15 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
168	20, 90, 167	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ph -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
169	166, 168	eqtrid 2276	. . . . . . . . . . . . 13 |- ( ph -> ( F ` K ) = ( N + 1 ) )
170	169	fveq2d 5643	. . . . . . . . . . . 12 |- ( ph -> ( G ` ( F ` K ) ) = ( G ` ( N + 1 ) ) )
171	165, 170	eqtr2d 2265	. . . . . . . . . . 11 |- ( ph -> ( G ` ( N + 1 ) ) = ( ( G o. F ) ` K ) )
172	171	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( G ` ( N + 1 ) ) = ( ( G o. F ) ` K ) )
173	163, 172	oveq12d 6036	. . . . . . . . 9 |- ( ( ph /\ K e. ( M ... N ) ) -> ( ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) = ( ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) .+ ( ( G o. F ) ` K ) ) )
174	112, 173	eqtr4d 2267	. . . . . . . 8 |- ( ( ph /\ K e. ( M ... N ) ) -> ( ( ( G o. F ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
175	103, 174	syldan 282	. . . . . . 7 |- ( ( ph /\ K = M ) -> ( ( ( G o. F ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
176	99	seqeq1d 10716	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
177	176	fveq1d 5641	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
178	177	oveq1d 6033	. . . . . . 7 |- ( ( ph /\ K = M ) -> ( ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
179	98, 175, 178	3eqtrd 2268	. . . . . 6 |- ( ( ph /\ K = M ) -> ( ( seq M ( .+ , ( G o. F ) ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
180		elfzuz 10256	. . . . . . . . . . 11 |- ( K e. ( ( M + 1 ) ... N ) -> K e. ( ZZ>= ` ( M + 1 ) ) )
181		eluzp1m1 9780	. . . . . . . . . . 11 |- ( ( M e. ZZ /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( K - 1 ) e. ( ZZ>= ` M ) )
182	8, 180, 181	syl2an 289	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( K - 1 ) e. ( ZZ>= ` M ) )
183	10	zcnd 9603	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. CC )
184		ax-1cn 8125	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
185		pncan 8385	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
186	183, 184, 185	sylancl 413	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
187		elfzelz 10260	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ZZ )
188		peano2zm 9517	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ZZ -> ( K - 1 ) e. ZZ )
189	92, 187, 188	3syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( K - 1 ) e. ZZ )
190		elfzuz3 10257	. . . . . . . . . . . . . . . . . . . . 21 |- ( K e. ( M ... ( N + 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` K ) )
191	92, 190	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` K ) )
192	93	zcnd 9603	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> K e. CC )
193		npcan 8388	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
194	192, 184, 193	sylancl 413	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( K - 1 ) + 1 ) = K )
195	194	fveq2d 5643	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
196	191, 195	eleqtrrd 2311	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
197		eluzp1m1 9780	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( K - 1 ) e. ZZ /\ ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) ) -> ( ( N + 1 ) - 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
198	189, 196, 197	syl2anc 411	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( N + 1 ) - 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
199	186, 198	eqeltrrd 2309	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. ( ZZ>= ` ( K - 1 ) ) )
200		fzss2 10299	. . . . . . . . . . . . . . . . 17 |- ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( M ... ( K - 1 ) ) C_ ( M ... N ) )
201	199, 200	syl 14	. . . . . . . . . . . . . . . 16 |- ( ph -> ( M ... ( K - 1 ) ) C_ ( M ... N ) )
202	201	sselda 3227	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... N ) )
203	202, 118	syldan 282	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) e. ( M ... N ) )
204	203	fvresd 5664	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
205		simpr 110	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. ( M ... N ) )
206	66	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( M ... N ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
207		fzelp1 10309	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( M ... N ) -> x e. ( M ... ( N + 1 ) ) )
208	207	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. ( M ... ( N + 1 ) ) )
209	128	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( M ... N ) ) -> ( x + 1 ) e. ( M ... ( N + 1 ) ) )
210		elfzelz 10260	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( M ... N ) -> x e. ZZ )
211	210, 93, 132	syl2anr 290	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( M ... N ) ) -> DECID x < K )
212	208, 209, 211	ifcldcd 3643	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( M ... N ) ) -> if ( x < K , x , ( x + 1 ) ) e. ( M ... ( N + 1 ) ) )
213	206, 212	ffvelcdmd 5783	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) e. ( M ... ( N + 1 ) ) )
214	21, 125, 205, 213	fvmptd3 5740	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
215	202, 214	syldan 282	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
216		elfzm11 10326	. . . . . . . . . . . . . . . . . . 19 |- ( ( M e. ZZ /\ K e. ZZ ) -> ( x e. ( M ... ( K - 1 ) ) <-> ( x e. ZZ /\ M <_ x /\ x < K ) ) )
217	8, 93, 216	syl2anc 411	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( x e. ( M ... ( K - 1 ) ) <-> ( x e. ZZ /\ M <_ x /\ x < K ) ) )
218	217	biimpa 296	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( x e. ZZ /\ M <_ x /\ x < K ) )
219	218	simp3d 1037	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x < K )
220		iftrue 3610	. . . . . . . . . . . . . . . . 17 |- ( x < K -> if ( x < K , x , ( x + 1 ) ) = x )
221	220	fveq2d 5643	. . . . . . . . . . . . . . . 16 |- ( x < K -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
222	219, 221	syl 14	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
223	215, 222	eqtrd 2264	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` x ) )
224	223	fveq2d 5643	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` x ) ) )
225	204, 224	eqtr2d 2265	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
226		peano2uz 9817	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
227		fzss2 10299	. . . . . . . . . . . . . . 15 |- ( ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) -> ( M ... ( K - 1 ) ) C_ ( M ... ( N + 1 ) ) )
228	199, 226, 227	3syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( M ... ( K - 1 ) ) C_ ( M ... ( N + 1 ) ) )
229	228	sselda 3227	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
230		fvco3 5717	. . . . . . . . . . . . . 14 |- ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
231	66, 230	sylan 283	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
232	229, 231	syldan 282	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
233	202, 152	syldan 282	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
234	225, 232, 233	3eqtr4d 2274	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
235	234	adantlr 477	. . . . . . . . . 10 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
236	19	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> .+ e. V )
237	94	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( G o. F ) e. _V )
238	27, 161	syl 14	. . . . . . . . . . 11 |- ( ph -> ( ( G |` ( M ... N ) ) o. J ) e. _V )
239	238	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( G |` ( M ... N ) ) o. J ) e. _V )
240	182, 235, 236, 237, 239	seqfveqg 10741	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) )
241		fzp1ss 10308	. . . . . . . . . . . 12 |- ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
242	6, 7, 241	3syl 17	. . . . . . . . . . 11 |- ( ph -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
243	242	sselda 3227	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. ( M ... N ) )
244	243, 174	syldan 282	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( ( G o. F ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
245	240, 244	oveq12d 6036	. . . . . . . 8 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( ( G o. F ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) ) )
246	229, 76	syldan 282	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
247	246	adantlr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
248	15	adantlr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
249	182, 247, 248, 237, 236	seqclg 10735	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) e. S )
250	74, 92	ffvelcdmd 5783	. . . . . . . . . . . 12 |- ( ph -> ( ( G o. F ) ` K ) e. C )
251	18, 250	sseldd 3228	. . . . . . . . . . 11 |- ( ph -> ( ( G o. F ) ` K ) e. S )
252	251	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( G o. F ) ` K ) e. S )
253	110	sselda 3227	. . . . . . . . . . . . 13 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( ( K + 1 ) ... ( N + 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
254	253, 77	syldan 282	. . . . . . . . . . . 12 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( ( K + 1 ) ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
255	62, 254, 57, 70, 63	seqclg 10735	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) e. S )
256	243, 255	syldan 282	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) e. S )
257	249, 252, 256	3jca 1203	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) e. S /\ ( ( G o. F ) ` K ) e. S /\ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) e. S ) )
258	17	caovassg 6181	. . . . . . . . 9 |- ( ( ph /\ ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) e. S /\ ( ( G o. F ) ` K ) e. S /\ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) e. S ) ) -> ( ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( G o. F ) ` K ) ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( ( G o. F ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) ) )
259	257, 258	syldan 282	. . . . . . . 8 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( G o. F ) ` K ) ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( ( G o. F ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) ) )
260	1, 18	fssd 5495	. . . . . . . . . . . . . . . 16 |- ( ph -> G : ( M ... ( N + 1 ) ) --> S )
261		fssres 5512	. . . . . . . . . . . . . . . 16 |- ( ( G : ( M ... ( N + 1 ) ) --> S /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) : ( M ... N ) --> S )
262	260, 3, 261	sylancl 413	. . . . . . . . . . . . . . 15 |- ( ph -> ( G |` ( M ... N ) ) : ( M ... N ) --> S )
263		fco 5500	. . . . . . . . . . . . . . 15 |- ( ( ( G |` ( M ... N ) ) : ( M ... N ) --> S /\ J : ( M ... N ) --> ( M ... N ) ) -> ( ( G |` ( M ... N ) ) o. J ) : ( M ... N ) --> S )
264	262, 25, 263	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G |` ( M ... N ) ) o. J ) : ( M ... N ) --> S )
265	264	ffvelcdmda 5782	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
266	202, 265	syldan 282	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
267	266	adantlr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
268	182, 267, 248, 239, 236	seqclg 10735	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) e. S )
269		elfzuz3 10257	. . . . . . . . . . . 12 |- ( K e. ( ( M + 1 ) ... N ) -> N e. ( ZZ>= ` K ) )
270	269	adantl 277	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> N e. ( ZZ>= ` K ) )
271	117, 265	syldan 282	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
272	271	adantlr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
273	270, 272, 248, 239, 236	seqclg 10735	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) e. S )
274	260, 90	ffvelcdmd 5783	. . . . . . . . . . 11 |- ( ph -> ( G ` ( N + 1 ) ) e. S )
275	274	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( G ` ( N + 1 ) ) e. S )
276	268, 273, 275	3jca 1203	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) e. S /\ ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) e. S /\ ( G ` ( N + 1 ) ) e. S ) )
277	17	caovassg 6181	. . . . . . . . 9 |- ( ( ph /\ ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) e. S /\ ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) e. S /\ ( G ` ( N + 1 ) ) e. S ) ) -> ( ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) ) .+ ( G ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) ) )
278	276, 277	syldan 282	. . . . . . . 8 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) ) .+ ( G ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) ) )
279	245, 259, 278	3eqtr4d 2274	. . . . . . 7 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( G o. F ) ` K ) ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) ) .+ ( G ` ( N + 1 ) ) ) )
280	8	adantr 276	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> M e. ZZ )
281	180	adantl 277	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. ( ZZ>= ` ( M + 1 ) ) )
282	280, 281, 236, 237	seqm1g 10737	. . . . . . . 8 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( G o. F ) ` K ) ) )
283	282	oveq1d 6033	. . . . . . 7 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( seq M ( .+ , ( G o. F ) ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( G o. F ) ` K ) ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) )
284	17	adantlr 477	. . . . . . . . . 10 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
285		elfzelz 10260	. . . . . . . . . . . . . . 15 |- ( K e. ( ( M + 1 ) ... N ) -> K e. ZZ )
286	285	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. ZZ )
287	286	zcnd 9603	. . . . . . . . . . . . 13 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. CC )
288	287, 184, 193	sylancl 413	. . . . . . . . . . . 12 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( K - 1 ) + 1 ) = K )
289	288	fveq2d 5643	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
290	270, 289	eleqtrrd 2311	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> N e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
291	265	adantlr 477	. . . . . . . . . 10 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
292	248, 284, 290, 236, 239, 182, 291	seqsplitg 10752	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( seq ( ( K - 1 ) + 1 ) ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) ) )
293	288	seqeq1d 10716	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> seq ( ( K - 1 ) + 1 ) ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
294	293	fveq1d 5641	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq ( ( K - 1 ) + 1 ) ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
295	294	oveq2d 6034	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( seq ( ( K - 1 ) + 1 ) ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) ) )
296	292, 295	eqtrd 2264	. . . . . . . 8 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) ) )
297	296	oveq1d 6033	. . . . . . 7 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) = ( ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) .+ ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) ) .+ ( G ` ( N + 1 ) ) ) )
298	279, 283, 297	3eqtr4d 2274	. . . . . 6 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( seq M ( .+ , ( G o. F ) ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
299	179, 298	jaodan 804	. . . . 5 |- ( ( ph /\ ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) -> ( ( seq M ( .+ , ( G o. F ) ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
300	81, 299	syldan 282	. . . 4 |- ( ( ph /\ K e. ( M ... N ) ) -> ( ( seq M ( .+ , ( G o. F ) ) ` K ) .+ ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
301	78, 300	eqtrd 2264	. . 3 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
302	6	adantr 276	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> N e. ( ZZ>= ` M ) )
303	94	adantr 276	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( G o. F ) e. _V )
304	19	adantr 276	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> .+ e. V )
305		seqp1g 10729	. . . . 5 |- ( ( N e. ( ZZ>= ` M ) /\ ( G o. F ) e. _V /\ .+ e. V ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` N ) .+ ( ( G o. F ) ` ( N + 1 ) ) ) )
306	302, 303, 304, 305	syl3anc 1273	. . . 4 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` N ) .+ ( ( G o. F ) ` ( N + 1 ) ) ) )
307	214	adantlr 477	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
308	210	zred 9602	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x e. RR )
309	308	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
310	10	zred 9602	. . . . . . . . . . . . . . 15 |- ( ph -> N e. RR )
311	310	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
312		peano2re 8315	. . . . . . . . . . . . . . 15 |- ( N e. RR -> ( N + 1 ) e. RR )
313	311, 312	syl 14	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) e. RR )
314		elfzle2 10263	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x <_ N )
315	314	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
316	311	ltp1d 9110	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
317	309, 311, 313, 315, 316	lelttrd 8304	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
318	317	adantlr 477	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
319		simplr 529	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K = ( N + 1 ) )
320	318, 319	breqtrrd 4116	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x < K )
321	320, 221	syl 14	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
322	307, 321	eqtrd 2264	. . . . . . . . 9 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` x ) )
323	322	fveq2d 5643	. . . . . . . 8 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( ( G |` ( M ... N ) ) ` ( F ` x ) ) )
324	66	ad2antrr 488	. . . . . . . . . . . . 13 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
325	207	adantl 277	. . . . . . . . . . . . 13 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x e. ( M ... ( N + 1 ) ) )
326	324, 325	ffvelcdmd 5783	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... ( N + 1 ) ) )
327	326	elfzelzd 10261	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ZZ )
328	6	ad2antrr 488	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> N e. ( ZZ>= ` M ) )
329	328, 7	syl 14	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> M e. ZZ )
330	328, 9	syl 14	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> N e. ZZ )
331		fzdcel 10275	. . . . . . . . . . 11 |- ( ( ( F ` x ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> DECID ( F ` x ) e. ( M ... N ) )
332	327, 329, 330, 331	syl3anc 1273	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> DECID ( F ` x ) e. ( M ... N ) )
333	308	adantl 277	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x e. RR )
334	333, 320	gtned 8292	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K =/= x )
335		elfzp1 10307	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` M ) -> ( ( F ` x ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) ) )
336	328, 335	syl 14	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) ) )
337	326, 336	mpbid 147	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) )
338	337	ord 731	. . . . . . . . . . . . 13 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( -. ( F ` x ) e. ( M ... N ) -> ( F ` x ) = ( N + 1 ) ) )
339	20	ad2antrr 488	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
340		f1ocnvfv 5920	. . . . . . . . . . . . . . 15 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( F ` x ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = x ) )
341	339, 325, 340	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = x ) )
342	22	eqeq1i 2239	. . . . . . . . . . . . . 14 |- ( K = x <-> ( `' F ` ( N + 1 ) ) = x )
343	341, 342	imbitrrdi 162	. . . . . . . . . . . . 13 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) = ( N + 1 ) -> K = x ) )
344	338, 343	syld 45	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( -. ( F ` x ) e. ( M ... N ) -> K = x ) )
345	344	a1d 22	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> (DECID ( F ` x ) e. ( M ... N ) -> ( -. ( F ` x ) e. ( M ... N ) -> K = x ) ) )
346	345	necon1addc 2478	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> (DECID ( F ` x ) e. ( M ... N ) -> ( K =/= x -> ( F ` x ) e. ( M ... N ) ) ) )
347	332, 334, 346	mp2d 47	. . . . . . . . 9 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... N ) )
348	347	fvresd 5664	. . . . . . . 8 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
349	323, 348	eqtr2d 2265	. . . . . . 7 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
350	66, 207, 230	syl2an 289	. . . . . . . 8 |- ( ( ph /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
351	350	adantlr 477	. . . . . . 7 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
352	152	adantlr 477	. . . . . . 7 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
353	349, 351, 352	3eqtr4d 2274	. . . . . 6 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
354	238	adantr 276	. . . . . 6 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( G |` ( M ... N ) ) o. J ) e. _V )
355	302, 353, 304, 303, 354	seqfveqg 10741	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
356		fvco3 5717	. . . . . . . 8 |- ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
357	66, 90, 356	syl2anc 411	. . . . . . 7 |- ( ph -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
358	357	adantr 276	. . . . . 6 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
359		simpr 110	. . . . . . . . . 10 |- ( ( ph /\ K = ( N + 1 ) ) -> K = ( N + 1 ) )
360	22, 359	eqtr3id 2278	. . . . . . . . 9 |- ( ( ph /\ K = ( N + 1 ) ) -> ( `' F ` ( N + 1 ) ) = ( N + 1 ) )
361	360	fveq2d 5643	. . . . . . . 8 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( F ` ( N + 1 ) ) )
362	168	adantr 276	. . . . . . . 8 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
363	361, 362	eqtr3d 2266	. . . . . . 7 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( N + 1 ) ) = ( N + 1 ) )
364	363	fveq2d 5643	. . . . . 6 |- ( ( ph /\ K = ( N + 1 ) ) -> ( G ` ( F ` ( N + 1 ) ) ) = ( G ` ( N + 1 ) ) )
365	358, 364	eqtrd 2264	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( N + 1 ) ) )
366	355, 365	oveq12d 6036	. . . 4 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( seq M ( .+ , ( G o. F ) ) ` N ) .+ ( ( G o. F ) ` ( N + 1 ) ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
367	306, 366	eqtrd 2264	. . 3 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
368		elfzp1 10307	. . . . 5 |- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... ( N + 1 ) ) <-> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) ) )
369	6, 368	syl 14	. . . 4 |- ( ph -> ( K e. ( M ... ( N + 1 ) ) <-> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) ) )
370	92, 369	mpbid 147	. . 3 |- ( ph -> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) )
371	301, 367, 370	mpjaodan 805	. 2 |- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
372		seqp1g 10729	. . 3 |- ( ( N e. ( ZZ>= ` M ) /\ G e. _V /\ .+ e. V ) -> ( seq M ( .+ , G ) ` ( N + 1 ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
373	6, 51, 19, 372	syl3anc 1273	. 2 |- ( ph -> ( seq M ( .+ , G ) ` ( N + 1 ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
374	56, 371, 373	3eqtr4d 2274	1 |- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( seq M ( .+ , G ) ` ( N + 1 ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 715  DECID wdc 841   /\ w3a 1004   A.wal 1395   = wceq 1397   e. wcel 2202   =/= wne 2402   _Vcvv 2802   C_ wss 3200   ifcif 3605   class class class wbr 4088   |-> cmpt 4150   `'ccnv 4724   |` cres 4727   o. ccom 4729   Fn wfn 5321   -->wf 5322   -1-1-onto->wf1o 5325   ` cfv 5326  (class class class)co 6018   Fincfn 6909   CCcc 8030   RRcr 8031   1c1 8033   + caddc 8035   < clt 8214   <_ cle 8215   - cmin 8350   ZZcz 9479   ZZ>=cuz 9755   ...cfz 10243   seqcseq 10710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4204  ax-sep 4207  ax-nul 4215  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-iinf 4686  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-mulrcl 8131  ax-addcom 8132  ax-mulcom 8133  ax-addass 8134  ax-mulass 8135  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-1rid 8139  ax-0id 8140  ax-rnegex 8141  ax-precex 8142  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-apti 8147  ax-pre-ltadd 8148  ax-pre-mulgt0 8149

This theorem depends on definitions:  df-bi 117  df-stab 838  df-dc 842  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-if 3606  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-tr 4188  df-id 4390  df-iord 4463  df-on 4465  df-ilim 4466  df-suc 4468  df-iom 4689  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-1st 6303  df-2nd 6304  df-recs 6471  df-frec 6557  df-1o 6582  df-er 6702  df-en 6910  df-fin 6912  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-reap 8755  df-ap 8762  df-inn 9144  df-n0 9403  df-z 9480  df-uz 9756  df-fz 10244  df-fzo 10378  df-seqfrec 10711

This theorem is referenced by:  seqf1og  10784