Theorem seqf1oglem2 10614

Description: Lemma for seqf1og 10615. (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 5409	. . . . . . . . 9 |- ( ph -> G Fn ( M ... ( N + 1 ) ) )
3		fzssp1 10144	. . . . . . . . 9 |- ( M ... N ) C_ ( M ... ( N + 1 ) )
4		fnssres 5372	. . . . . . . . 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 9608	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
8	6, 7	syl 14	. . . . . . . . 9 |- ( ph -> M e. ZZ )
9		eluzelz 9612	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
10	6, 9	syl 14	. . . . . . . . 9 |- ( ph -> N e. ZZ )
11	8, 10	fzfigd 10525	. . . . . . . 8 |- ( ph -> ( M ... N ) e. Fin )
12		fnfi 7003	. . . . . . . 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 2776	. . . . . 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 10613	. . . . . . . 8 |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
24		f1of 5505	. . . . . . . 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 5793	. . . . . 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 5434	. . . . . . 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 5493	. . . . . . . 8 |- ( f = J -> ( f : ( M ... N ) -1-1-onto-> ( M ... N ) <-> J : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
33		feq1 5391	. . . . . . . 8 |- ( g = ( G |` ( M ... N ) ) -> ( g : ( M ... N ) --> C <-> ( G |` ( M ... N ) ) : ( M ... N ) --> C ) )
34	32, 33	bi2anan9r 607	. . . . . . 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 4824	. . . . . . . . . . 11 |- ( g = ( G |` ( M ... N ) ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. f ) )
36		coeq2 4825	. . . . . . . . . . 11 |- ( f = J -> ( ( G |` ( M ... N ) ) o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
37	35, 36	sylan9eq 2249	. . . . . . . . . 10 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
38	37	seqeq3d 10549	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , ( g o. f ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
39	38	fveq1d 5561	. . . . . . . 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 10549	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , g ) = seq M ( .+ , ( G |` ( M ... N ) ) ) )
42	41	fveq1d 5561	. . . . . . . 8 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , g ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
43	39, 42	eqeq12d 2211	. . . . . . 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 2855	. . . . 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 5583	. . . . . 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 9453	. . . . . . . 8 |- ( ph -> ( N + 1 ) e. ZZ )
50	8, 49	fzfigd 10525	. . . . . . 7 |- ( ph -> ( M ... ( N + 1 ) ) e. Fin )
51	1, 50	fexd 5793	. . . . . 6 |- ( ph -> G e. _V )
52		resexg 4987	. . . . . 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 10572	. . . 4 |- ( ph -> ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
55	46, 54	eqtrd 2229	. . 3 |- ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
56	55	oveq1d 5938	. 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 10099	. . . . . . 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 9629	. . . . . 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 5505	. . . . . . . . 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 5793	. . . . . . 7 |- ( ph -> F e. _V )
68	67	adantr 276	. . . . . 6 |- ( ( ph /\ K e. ( M ... N ) ) -> F e. _V )
69		coexg 5215	. . . . . 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 10098	. . . . . 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 5424	. . . . . . . . 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 5421	. . . . . . 7 |- ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> S )
76	75	ffvelcdmda 5698	. . . . . 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 10583	. . . 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 10176	. . . . . . 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 10544	. . . . . . . . . . 11 |- ( K = M -> seq K ( .+ , ( G o. F ) ) = seq M ( .+ , ( G o. F ) ) )
83	82	eqcomd 2202	. . . . . . . . . 10 |- ( K = M -> seq M ( .+ , ( G o. F ) ) = seq K ( .+ , ( G o. F ) ) )
84	83	fveq1d 5561	. . . . . . . . 9 |- ( K = M -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( seq K ( .+ , ( G o. F ) ) ` K ) )
85		f1ocnv 5518	. . . . . . . . . . . . . 14 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
86		f1of 5505	. . . . . . . . . . . . . 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 9659	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
89		eluzfz2 10109	. . . . . . . . . . . . . 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 5699	. . . . . . . . . . . 12 |- ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
92	22, 91	eqeltrid 2283	. . . . . . . . . . 11 |- ( ph -> K e. ( M ... ( N + 1 ) ) )
93	92	elfzelzd 10103	. . . . . . . . . 10 |- ( ph -> K e. ZZ )
94	51, 67, 69	syl2anc 411	. . . . . . . . . 10 |- ( ph -> ( G o. F ) e. _V )
95		seq1g 10557	. . . . . . . . . 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 1249	. . . . . . . . 9 |- ( ph -> ( seq K ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
97	84, 96	sylan9eqr 2251	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
98	97	oveq1d 5938	. . . . . . 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 10108	. . . . . . . . . . 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 2273	. . . . . . . 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 9659	. . . . . . . . . . 11 |- ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
109		fzss1 10140	. . . . . . . . . . 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 10612	. . . . . . . . 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 9355	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( M ... N ) ) -> 1 e. ZZ )
114		elfzuz 10098	. . . . . . . . . . . . . . . . . 18 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ( ZZ>= ` M ) )
115		fzss1 10140	. . . . . . . . . . . . . . . . . 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 3184	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... N ) )
118	25	ffvelcdmda 5698	. . . . . . . . . . . . . . . 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 5584	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
121		breq1 4037	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> ( k < K <-> x < K ) )
122		id 19	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> k = x )
123		oveq1 5930	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> ( k + 1 ) = ( x + 1 ) )
124	121, 122, 123	ifbieq12d 3588	. . . . . . . . . . . . . . . . . 18 |- ( k = x -> if ( k < K , k , ( k + 1 ) ) = if ( x < K , x , ( x + 1 ) ) )
125	124	fveq2d 5563	. . . . . . . . . . . . . . . . 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 3182	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... ( N + 1 ) ) )
128		fzp1elp1 10152	. . . . . . . . . . . . . . . . . . . 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 10103	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
131	93	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. ZZ )
132		zdclt 9405	. . . . . . . . . . . . . . . . . . . 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 3598	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> if ( x < K , x , ( x + 1 ) ) e. ( M ... ( N + 1 ) ) )
135	126, 134	ffvelcdmd 5699	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) e. ( M ... ( N + 1 ) ) )
136	21, 125, 117, 135	fvmptd3 5656	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
137	93	zred 9450	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. RR )
138	137	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. RR )
139		elfzelz 10102	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( K ... N ) -> x e. ZZ )
140	139	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
141	140	zred 9450	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. RR )
142		elfzle1 10104	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( K ... N ) -> K <_ x )
143	142	adantl 277	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K <_ x )
144	138, 141, 143	lensymd 8150	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> -. x < K )
145		iffalse 3570	. . . . . . . . . . . . . . . . . 18 |- ( -. x < K -> if ( x < K , x , ( x + 1 ) ) = ( x + 1 ) )
146	145	fveq2d 5563	. . . . . . . . . . . . . . . . 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 2229	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` ( x + 1 ) ) )
149	148	fveq2d 5563	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
150	120, 149	eqtrd 2229	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
151		fvco3 5633	. . . . . . . . . . . . . . 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 5633	. . . . . . . . . . . . . . 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 2239	. . . . . . . . . . . 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 5215	. . . . . . . . . . . 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 10576	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) )
164		fvco3 5633	. . . . . . . . . . . . 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 5562	. . . . . . . . . . . . . 14 |- ( F ` K ) = ( F ` ( `' F ` ( N + 1 ) ) )
167		f1ocnvfv2 5826	. . . . . . . . . . . . . . 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 2241	. . . . . . . . . . . . 13 |- ( ph -> ( F ` K ) = ( N + 1 ) )
170	169	fveq2d 5563	. . . . . . . . . . . 12 |- ( ph -> ( G ` ( F ` K ) ) = ( G ` ( N + 1 ) ) )
171	165, 170	eqtr2d 2230	. . . . . . . . . . 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 5941	. . . . . . . . 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 2232	. . . . . . . 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 10547	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
177	176	fveq1d 5561	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
178	177	oveq1d 5938	. . . . . . 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 2233	. . . . . 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 10098	. . . . . . . . . . 11 |- ( K e. ( ( M + 1 ) ... N ) -> K e. ( ZZ>= ` ( M + 1 ) ) )
181		eluzp1m1 9627	. . . . . . . . . . 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 9451	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. CC )
184		ax-1cn 7974	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
185		pncan 8234	. . . . . . . . . . . . . . . . . . 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 10102	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ZZ )
188		peano2zm 9366	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ZZ -> ( K - 1 ) e. ZZ )
189	92, 187, 188	3syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( K - 1 ) e. ZZ )
190		elfzuz3 10099	. . . . . . . . . . . . . . . . . . . . 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 9451	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> K e. CC )
193		npcan 8237	. . . . . . . . . . . . . . . . . . . . . 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 5563	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
196	191, 195	eleqtrrd 2276	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
197		eluzp1m1 9627	. . . . . . . . . . . . . . . . . . 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 2274	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. ( ZZ>= ` ( K - 1 ) ) )
200		fzss2 10141	. . . . . . . . . . . . . . . . 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 3184	. . . . . . . . . . . . . . 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 5584	. . . . . . . . . . . . 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 10151	. . . . . . . . . . . . . . . . . . . 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 10102	. . . . . . . . . . . . . . . . . . . 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 3598	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( M ... N ) ) -> if ( x < K , x , ( x + 1 ) ) e. ( M ... ( N + 1 ) ) )
213	206, 212	ffvelcdmd 5699	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) e. ( M ... ( N + 1 ) ) )
214	21, 125, 205, 213	fvmptd3 5656	. . . . . . . . . . . . . . . 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 10168	. . . . . . . . . . . . . . . . . . 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 1013	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x < K )
220		iftrue 3567	. . . . . . . . . . . . . . . . 17 |- ( x < K -> if ( x < K , x , ( x + 1 ) ) = x )
221	220	fveq2d 5563	. . . . . . . . . . . . . . . 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 2229	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` x ) )
224	223	fveq2d 5563	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` x ) ) )
225	204, 224	eqtr2d 2230	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
226		peano2uz 9659	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
227		fzss2 10141	. . . . . . . . . . . . . . 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 3184	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
230		fvco3 5633	. . . . . . . . . . . . . 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 2239	. . . . . . . . . . 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 10572	. . . . . . . . 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 10150	. . . . . . . . . . . 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 3184	. . . . . . . . . 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 5941	. . . . . . . 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 10566	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) e. S )
250	74, 92	ffvelcdmd 5699	. . . . . . . . . . . 12 |- ( ph -> ( ( G o. F ) ` K ) e. C )
251	18, 250	sseldd 3185	. . . . . . . . . . 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 3184	. . . . . . . . . . . . 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 10566	. . . . . . . . . . 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 1179	. . . . . . . . 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 6083	. . . . . . . . 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 5421	. . . . . . . . . . . . . . . 16 |- ( ph -> G : ( M ... ( N + 1 ) ) --> S )
261		fssres 5434	. . . . . . . . . . . . . . . 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 5424	. . . . . . . . . . . . . . 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 5698	. . . . . . . . . . . . 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 10566	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) e. S )
269		elfzuz3 10099	. . . . . . . . . . . 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 10566	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) e. S )
274	260, 90	ffvelcdmd 5699	. . . . . . . . . . 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 1179	. . . . . . . . 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 6083	. . . . . . . . 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 2239	. . . . . . 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 10568	. . . . . . . 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 5938	. . . . . . 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 10102	. . . . . . . . . . . . . . 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 9451	. . . . . . . . . . . . 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 5563	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
290	270, 289	eleqtrrd 2276	. . . . . . . . . 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 10583	. . . . . . . . 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 10547	. . . . . . . . . . 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 5561	. . . . . . . . . 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 5939	. . . . . . . . 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 2229	. . . . . . . 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 5938	. . . . . . 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 2239	. . . . . 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 798	. . . . 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 2229	. . 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 10560	. . . . 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 1249	. . . 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 9450	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x e. RR )
309	308	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
310	10	zred 9450	. . . . . . . . . . . . . . 15 |- ( ph -> N e. RR )
311	310	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
312		peano2re 8164	. . . . . . . . . . . . . . 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 10105	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x <_ N )
315	314	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
316	311	ltp1d 8959	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
317	309, 311, 313, 315, 316	lelttrd 8153	. . . . . . . . . . . . 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 528	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K = ( N + 1 ) )
320	318, 319	breqtrrd 4062	. . . . . . . . . . 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 2229	. . . . . . . . 9 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` x ) )
323	322	fveq2d 5563	. . . . . . . 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 5699	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... ( N + 1 ) ) )
327	326	elfzelzd 10103	. . . . . . . . . . 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 10117	. . . . . . . . . . 11 |- ( ( ( F ` x ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> DECID ( F ` x ) e. ( M ... N ) )
332	327, 329, 330, 331	syl3anc 1249	. . . . . . . . . 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 8141	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K =/= x )
335		elfzp1 10149	. . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . 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 5827	. . . . . . . . . . . . . . 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 2204	. . . . . . . . . . . . . 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 2443	. . . . . . . . . 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 5584	. . . . . . . 8 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
349	323, 348	eqtr2d 2230	. . . . . . 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 2239	. . . . . 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 10572	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
356		fvco3 5633	. . . . . . . 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 2243	. . . . . . . . 9 |- ( ( ph /\ K = ( N + 1 ) ) -> ( `' F ` ( N + 1 ) ) = ( N + 1 ) )
361	360	fveq2d 5563	. . . . . . . 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 2231	. . . . . . 7 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( N + 1 ) ) = ( N + 1 ) )
364	363	fveq2d 5563	. . . . . 6 |- ( ( ph /\ K = ( N + 1 ) ) -> ( G ` ( F ` ( N + 1 ) ) ) = ( G ` ( N + 1 ) ) )
365	358, 364	eqtrd 2229	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( N + 1 ) ) )
366	355, 365	oveq12d 5941	. . . 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 2229	. . 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 10149	. . . . 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 799	. 2 |- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
372		seqp1g 10560	. . 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 1249	. 2 |- ( ph -> ( seq M ( .+ , G ) ` ( N + 1 ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
374	56, 371, 373	3eqtr4d 2239	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 709  DECID wdc 835   /\ w3a 980   A.wal 1362   = wceq 1364   e. wcel 2167   =/= wne 2367   _Vcvv 2763   C_ wss 3157   ifcif 3562   class class class wbr 4034   |-> cmpt 4095   `'ccnv 4663   |` cres 4666   o. ccom 4668   Fn wfn 5254   -->wf 5255   -1-1-onto->wf1o 5258   ` cfv 5259  (class class class)co 5923   Fincfn 6800   CCcc 7879   RRcr 7880   1c1 7882   + caddc 7884   < clt 8063   <_ cle 8064   - cmin 8199   ZZcz 9328   ZZ>=cuz 9603   ...cfz 10085   seqcseq 10541

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4149  ax-sep 4152  ax-nul 4160  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-iinf 4625  ax-cnex 7972  ax-resscn 7973  ax-1cn 7974  ax-1re 7975  ax-icn 7976  ax-addcl 7977  ax-addrcl 7978  ax-mulcl 7979  ax-mulrcl 7980  ax-addcom 7981  ax-mulcom 7982  ax-addass 7983  ax-mulass 7984  ax-distr 7985  ax-i2m1 7986  ax-0lt1 7987  ax-1rid 7988  ax-0id 7989  ax-rnegex 7990  ax-precex 7991  ax-cnre 7992  ax-pre-ltirr 7993  ax-pre-ltwlin 7994  ax-pre-lttrn 7995  ax-pre-apti 7996  ax-pre-ltadd 7997  ax-pre-mulgt0 7998

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3452  df-if 3563  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-iun 3919  df-br 4035  df-opab 4096  df-mpt 4097  df-tr 4133  df-id 4329  df-iord 4402  df-on 4404  df-ilim 4405  df-suc 4407  df-iom 4628  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266  df-fv 5267  df-riota 5878  df-ov 5926  df-oprab 5927  df-mpo 5928  df-1st 6199  df-2nd 6200  df-recs 6364  df-frec 6450  df-1o 6475  df-er 6593  df-en 6801  df-fin 6803  df-pnf 8065  df-mnf 8066  df-xr 8067  df-ltxr 8068  df-le 8069  df-sub 8201  df-neg 8202  df-reap 8604  df-ap 8611  df-inn 8993  df-n0 9252  df-z 9329  df-uz 9604  df-fz 10086  df-fzo 10220  df-seqfrec 10542

This theorem is referenced by:  seqf1og  10615