Theorem seqf1oglem2 10881

Description: Lemma for seqf1og 10882. (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 5508	. . . . . . . . 9 |- ( ph -> G Fn ( M ... ( N + 1 ) ) )
3		fzssp1 10400	. . . . . . . . 9 |- ( M ... N ) C_ ( M ... ( N + 1 ) )
4		fnssres 5470	. . . . . . . . 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 9857	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
8	6, 7	syl 14	. . . . . . . . 9 |- ( ph -> M e. ZZ )
9		eluzelz 9862	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
10	6, 9	syl 14	. . . . . . . . 9 |- ( ph -> N e. ZZ )
11	8, 10	fzfigd 10792	. . . . . . . 8 |- ( ph -> ( M ... N ) e. Fin )
12		fnfi 7202	. . . . . . . 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 2826	. . . . . 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 10880	. . . . . . . 8 |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
24		f1of 5613	. . . . . . . 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 5915	. . . . . 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 5539	. . . . . . 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 5601	. . . . . . . 8 |- ( f = J -> ( f : ( M ... N ) -1-1-onto-> ( M ... N ) <-> J : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
33		feq1 5490	. . . . . . . 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 4911	. . . . . . . . . . 11 |- ( g = ( G |` ( M ... N ) ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. f ) )
36		coeq2 4912	. . . . . . . . . . 11 |- ( f = J -> ( ( G |` ( M ... N ) ) o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
37	35, 36	sylan9eq 2285	. . . . . . . . . 10 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
38	37	seqeq3d 10816	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , ( g o. f ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
39	38	fveq1d 5671	. . . . . . . 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 10816	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , g ) = seq M ( .+ , ( G |` ( M ... N ) ) ) )
42	41	fveq1d 5671	. . . . . . . 8 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , g ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
43	39, 42	eqeq12d 2247	. . . . . . 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 2907	. . . . 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 5693	. . . . . 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 9702	. . . . . . . 8 |- ( ph -> ( N + 1 ) e. ZZ )
50	8, 49	fzfigd 10792	. . . . . . 7 |- ( ph -> ( M ... ( N + 1 ) ) e. Fin )
51	1, 50	fexd 5915	. . . . . 6 |- ( ph -> G e. _V )
52		resexg 5077	. . . . . 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 10839	. . . 4 |- ( ph -> ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
55	46, 54	eqtrd 2265	. . 3 |- ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
56	55	oveq1d 6064	. 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 10355	. . . . . . 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 9879	. . . . . 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 5613	. . . . . . . . 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 5915	. . . . . . 7 |- ( ph -> F e. _V )
68	67	adantr 276	. . . . . 6 |- ( ( ph /\ K e. ( M ... N ) ) -> F e. _V )
69		coexg 5306	. . . . . 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 10354	. . . . . 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 5526	. . . . . . . . 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 5521	. . . . . . 7 |- ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> S )
76	75	ffvelcdmda 5811	. . . . . 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 10850	. . . 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 10432	. . . . . . 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 10811	. . . . . . . . . . 11 |- ( K = M -> seq K ( .+ , ( G o. F ) ) = seq M ( .+ , ( G o. F ) ) )
83	82	eqcomd 2238	. . . . . . . . . 10 |- ( K = M -> seq M ( .+ , ( G o. F ) ) = seq K ( .+ , ( G o. F ) ) )
84	83	fveq1d 5671	. . . . . . . . 9 |- ( K = M -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( seq K ( .+ , ( G o. F ) ) ` K ) )
85		f1ocnv 5626	. . . . . . . . . . . . . 14 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
86		f1of 5613	. . . . . . . . . . . . . 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 9914	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
89		eluzfz2 10365	. . . . . . . . . . . . . 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 5812	. . . . . . . . . . . 12 |- ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
92	22, 91	eqeltrid 2319	. . . . . . . . . . 11 |- ( ph -> K e. ( M ... ( N + 1 ) ) )
93	92	elfzelzd 10359	. . . . . . . . . 10 |- ( ph -> K e. ZZ )
94	51, 67, 69	syl2anc 411	. . . . . . . . . 10 |- ( ph -> ( G o. F ) e. _V )
95		seq1g 10824	. . . . . . . . . 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 1274	. . . . . . . . 9 |- ( ph -> ( seq K ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
97	84, 96	sylan9eqr 2287	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
98	97	oveq1d 6064	. . . . . . 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 10364	. . . . . . . . . . 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 2309	. . . . . . . 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 9914	. . . . . . . . . . 11 |- ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
109		fzss1 10396	. . . . . . . . . . 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 10879	. . . . . . . . 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 9603	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( M ... N ) ) -> 1 e. ZZ )
114		elfzuz 10354	. . . . . . . . . . . . . . . . . 18 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ( ZZ>= ` M ) )
115		fzss1 10396	. . . . . . . . . . . . . . . . . 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 3237	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... N ) )
118	25	ffvelcdmda 5811	. . . . . . . . . . . . . . . 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 5694	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
121		breq1 4111	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> ( k < K <-> x < K ) )
122		id 19	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> k = x )
123		oveq1 6056	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> ( k + 1 ) = ( x + 1 ) )
124	121, 122, 123	ifbieq12d 3648	. . . . . . . . . . . . . . . . . 18 |- ( k = x -> if ( k < K , k , ( k + 1 ) ) = if ( x < K , x , ( x + 1 ) ) )
125	124	fveq2d 5673	. . . . . . . . . . . . . . . . 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 3235	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... ( N + 1 ) ) )
128		fzp1elp1 10408	. . . . . . . . . . . . . . . . . . . 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 10359	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
131	93	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. ZZ )
132		zdclt 9654	. . . . . . . . . . . . . . . . . . . 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 3659	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> if ( x < K , x , ( x + 1 ) ) e. ( M ... ( N + 1 ) ) )
135	126, 134	ffvelcdmd 5812	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) e. ( M ... ( N + 1 ) ) )
136	21, 125, 117, 135	fvmptd3 5770	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
137	93	zred 9699	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. RR )
138	137	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. RR )
139		elfzelz 10358	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( K ... N ) -> x e. ZZ )
140	139	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
141	140	zred 9699	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. RR )
142		elfzle1 10360	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( K ... N ) -> K <_ x )
143	142	adantl 277	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K <_ x )
144	138, 141, 143	lensymd 8394	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> -. x < K )
145		iffalse 3629	. . . . . . . . . . . . . . . . . 18 |- ( -. x < K -> if ( x < K , x , ( x + 1 ) ) = ( x + 1 ) )
146	145	fveq2d 5673	. . . . . . . . . . . . . . . . 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 2265	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` ( x + 1 ) ) )
149	148	fveq2d 5673	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
150	120, 149	eqtrd 2265	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
151		fvco3 5747	. . . . . . . . . . . . . . 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 5747	. . . . . . . . . . . . . . 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 2275	. . . . . . . . . . . 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 5306	. . . . . . . . . . . 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 10843	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) )
164		fvco3 5747	. . . . . . . . . . . . 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 5672	. . . . . . . . . . . . . 14 |- ( F ` K ) = ( F ` ( `' F ` ( N + 1 ) ) )
167		f1ocnvfv2 5950	. . . . . . . . . . . . . . 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 2277	. . . . . . . . . . . . 13 |- ( ph -> ( F ` K ) = ( N + 1 ) )
170	169	fveq2d 5673	. . . . . . . . . . . 12 |- ( ph -> ( G ` ( F ` K ) ) = ( G ` ( N + 1 ) ) )
171	165, 170	eqtr2d 2266	. . . . . . . . . . 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 6067	. . . . . . . . 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 2268	. . . . . . . 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 10814	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
177	176	fveq1d 5671	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
178	177	oveq1d 6064	. . . . . . 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 2269	. . . . . 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 10354	. . . . . . . . . . 11 |- ( K e. ( ( M + 1 ) ... N ) -> K e. ( ZZ>= ` ( M + 1 ) ) )
181		eluzp1m1 9877	. . . . . . . . . . 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 9700	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. CC )
184		ax-1cn 8219	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
185		pncan 8478	. . . . . . . . . . . . . . . . . . 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 10358	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ZZ )
188		peano2zm 9614	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ZZ -> ( K - 1 ) e. ZZ )
189	92, 187, 188	3syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( K - 1 ) e. ZZ )
190		elfzuz3 10355	. . . . . . . . . . . . . . . . . . . . 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 9700	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> K e. CC )
193		npcan 8481	. . . . . . . . . . . . . . . . . . . . . 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 5673	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
196	191, 195	eleqtrrd 2312	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
197		eluzp1m1 9877	. . . . . . . . . . . . . . . . . . 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 2310	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. ( ZZ>= ` ( K - 1 ) ) )
200		fzss2 10397	. . . . . . . . . . . . . . . . 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 3237	. . . . . . . . . . . . . . 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 5694	. . . . . . . . . . . . 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 10407	. . . . . . . . . . . . . . . . . . . 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 10358	. . . . . . . . . . . . . . . . . . . 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 3659	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( M ... N ) ) -> if ( x < K , x , ( x + 1 ) ) e. ( M ... ( N + 1 ) ) )
213	206, 212	ffvelcdmd 5812	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) e. ( M ... ( N + 1 ) ) )
214	21, 125, 205, 213	fvmptd3 5770	. . . . . . . . . . . . . . . 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 10424	. . . . . . . . . . . . . . . . . . 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 1038	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x < K )
220		iftrue 3626	. . . . . . . . . . . . . . . . 17 |- ( x < K -> if ( x < K , x , ( x + 1 ) ) = x )
221	220	fveq2d 5673	. . . . . . . . . . . . . . . 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 2265	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` x ) )
224	223	fveq2d 5673	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` x ) ) )
225	204, 224	eqtr2d 2266	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
226		peano2uz 9914	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
227		fzss2 10397	. . . . . . . . . . . . . . 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 3237	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
230		fvco3 5747	. . . . . . . . . . . . . 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 2275	. . . . . . . . . . 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 10839	. . . . . . . . 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 10406	. . . . . . . . . . . 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 3237	. . . . . . . . . 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 6067	. . . . . . . 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 10833	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) e. S )
250	74, 92	ffvelcdmd 5812	. . . . . . . . . . . 12 |- ( ph -> ( ( G o. F ) ` K ) e. C )
251	18, 250	sseldd 3238	. . . . . . . . . . 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 3237	. . . . . . . . . . . . 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 10833	. . . . . . . . . . 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 1204	. . . . . . . . 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 6212	. . . . . . . . 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 5521	. . . . . . . . . . . . . . . 16 |- ( ph -> G : ( M ... ( N + 1 ) ) --> S )
261		fssres 5539	. . . . . . . . . . . . . . . 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 5526	. . . . . . . . . . . . . . 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 5811	. . . . . . . . . . . . 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 10833	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) e. S )
269		elfzuz3 10355	. . . . . . . . . . . 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 10833	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) e. S )
274	260, 90	ffvelcdmd 5812	. . . . . . . . . . 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 1204	. . . . . . . . 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 6212	. . . . . . . . 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 2275	. . . . . . 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 10835	. . . . . . . 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 6064	. . . . . . 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 10358	. . . . . . . . . . . . . . 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 9700	. . . . . . . . . . . . 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 5673	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
290	270, 289	eleqtrrd 2312	. . . . . . . . . 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 10850	. . . . . . . . 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 10814	. . . . . . . . . . 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 5671	. . . . . . . . . 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 6065	. . . . . . . . 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 2265	. . . . . . . 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 6064	. . . . . . 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 2275	. . . . . 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 805	. . . . 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 2265	. . 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 10827	. . . . 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 1274	. . . 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 9699	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x e. RR )
309	308	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
310	10	zred 9699	. . . . . . . . . . . . . . 15 |- ( ph -> N e. RR )
311	310	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
312		peano2re 8408	. . . . . . . . . . . . . . 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 10361	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x <_ N )
315	314	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
316	311	ltp1d 9203	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
317	309, 311, 313, 315, 316	lelttrd 8397	. . . . . . . . . . . . 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 4136	. . . . . . . . . . 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 2265	. . . . . . . . 9 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` x ) )
323	322	fveq2d 5673	. . . . . . . 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 5812	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... ( N + 1 ) ) )
327	326	elfzelzd 10359	. . . . . . . . . . 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 10373	. . . . . . . . . . 11 |- ( ( ( F ` x ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> DECID ( F ` x ) e. ( M ... N ) )
332	327, 329, 330, 331	syl3anc 1274	. . . . . . . . . 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 8385	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K =/= x )
335		elfzp1 10405	. . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . 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 5951	. . . . . . . . . . . . . . 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 2240	. . . . . . . . . . . . . 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 2488	. . . . . . . . . 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 5694	. . . . . . . 8 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
349	323, 348	eqtr2d 2266	. . . . . . 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 2275	. . . . . 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 10839	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
356		fvco3 5747	. . . . . . . 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 2279	. . . . . . . . 9 |- ( ( ph /\ K = ( N + 1 ) ) -> ( `' F ` ( N + 1 ) ) = ( N + 1 ) )
361	360	fveq2d 5673	. . . . . . . 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 2267	. . . . . . 7 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( N + 1 ) ) = ( N + 1 ) )
364	363	fveq2d 5673	. . . . . 6 |- ( ( ph /\ K = ( N + 1 ) ) -> ( G ` ( F ` ( N + 1 ) ) ) = ( G ` ( N + 1 ) ) )
365	358, 364	eqtrd 2265	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( N + 1 ) ) )
366	355, 365	oveq12d 6067	. . . 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 2265	. . 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 10405	. . . . 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 806	. 2 |- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
372		seqp1g 10827	. . 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 1274	. 2 |- ( ph -> ( seq M ( .+ , G ) ` ( N + 1 ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
374	56, 371, 373	3eqtr4d 2275	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 716  DECID wdc 842   /\ w3a 1005   A.wal 1396   = wceq 1398   e. wcel 2203   =/= wne 2412   _Vcvv 2812   C_ wss 3210   ifcif 3619   class class class wbr 4108   |-> cmpt 4170   `'ccnv 4747   |` cres 4750   o. ccom 4752   Fn wfn 5346   -->wf 5347   -1-1-onto->wf1o 5350   ` cfv 5351  (class class class)co 6049   Fincfn 6974   CCcc 8124   RRcr 8125   1c1 8127   + caddc 8129   < clt 8307   <_ cle 8308   - cmin 8443   ZZcz 9576   ZZ>=cuz 9852   ...cfz 10341   seqcseq 10808

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4224  ax-sep 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-iinf 4709  ax-cnex 8217  ax-resscn 8218  ax-1cn 8219  ax-1re 8220  ax-icn 8221  ax-addcl 8222  ax-addrcl 8223  ax-mulcl 8224  ax-mulrcl 8225  ax-addcom 8226  ax-mulcom 8227  ax-addass 8228  ax-mulass 8229  ax-distr 8230  ax-i2m1 8231  ax-0lt1 8232  ax-1rid 8233  ax-0id 8234  ax-rnegex 8235  ax-precex 8236  ax-cnre 8237  ax-pre-ltirr 8238  ax-pre-ltwlin 8239  ax-pre-lttrn 8240  ax-pre-apti 8241  ax-pre-ltadd 8242  ax-pre-mulgt0 8243

This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2814  df-sbc 3042  df-csb 3138  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-if 3620  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-int 3949  df-iun 3992  df-br 4109  df-opab 4171  df-mpt 4172  df-tr 4208  df-id 4413  df-iord 4486  df-on 4488  df-ilim 4489  df-suc 4491  df-iom 4712  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-iota 5311  df-fun 5353  df-fn 5354  df-f 5355  df-f1 5356  df-fo 5357  df-f1o 5358  df-fv 5359  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-1st 6333  df-2nd 6334  df-recs 6535  df-frec 6621  df-1o 6646  df-er 6766  df-en 6975  df-fin 6977  df-pnf 8309  df-mnf 8310  df-xr 8311  df-ltxr 8312  df-le 8313  df-sub 8445  df-neg 8446  df-reap 8848  df-ap 8855  df-inn 9237  df-n0 9496  df-z 9577  df-uz 9853  df-fz 10342  df-fzo 10476  df-seqfrec 10809

This theorem is referenced by:  seqf1og  10882