Theorem seqf1oglem2 10581

Description: Lemma for seqf1og 10582. (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 5396	. . . . . . . . 9 |- ( ph -> G Fn ( M ... ( N + 1 ) ) )
3		fzssp1 10123	. . . . . . . . 9 |- ( M ... N ) C_ ( M ... ( N + 1 ) )
4		fnssres 5359	. . . . . . . . 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 9587	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
8	6, 7	syl 14	. . . . . . . . 9 |- ( ph -> M e. ZZ )
9		eluzelz 9591	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
10	6, 9	syl 14	. . . . . . . . 9 |- ( ph -> N e. ZZ )
11	8, 10	fzfigd 10492	. . . . . . . 8 |- ( ph -> ( M ... N ) e. Fin )
12		fnfi 6985	. . . . . . . 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 2773	. . . . . 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 10580	. . . . . . . 8 |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
24		f1of 5492	. . . . . . . 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 5780	. . . . . 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 5421	. . . . . . 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 5480	. . . . . . . 8 |- ( f = J -> ( f : ( M ... N ) -1-1-onto-> ( M ... N ) <-> J : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
33		feq1 5378	. . . . . . . 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 4813	. . . . . . . . . . 11 |- ( g = ( G |` ( M ... N ) ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. f ) )
36		coeq2 4814	. . . . . . . . . . 11 |- ( f = J -> ( ( G |` ( M ... N ) ) o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
37	35, 36	sylan9eq 2246	. . . . . . . . . 10 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
38	37	seqeq3d 10516	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , ( g o. f ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
39	38	fveq1d 5548	. . . . . . . 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 10516	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , g ) = seq M ( .+ , ( G |` ( M ... N ) ) ) )
42	41	fveq1d 5548	. . . . . . . 8 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , g ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
43	39, 42	eqeq12d 2208	. . . . . . 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 2851	. . . . 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 5570	. . . . . 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 9432	. . . . . . . 8 |- ( ph -> ( N + 1 ) e. ZZ )
50	8, 49	fzfigd 10492	. . . . . . 7 |- ( ph -> ( M ... ( N + 1 ) ) e. Fin )
51	1, 50	fexd 5780	. . . . . 6 |- ( ph -> G e. _V )
52		resexg 4976	. . . . . 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 10539	. . . 4 |- ( ph -> ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
55	46, 54	eqtrd 2226	. . 3 |- ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
56	55	oveq1d 5925	. 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 10078	. . . . . . 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 9608	. . . . . 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 5492	. . . . . . . . 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 5780	. . . . . . 7 |- ( ph -> F e. _V )
68	67	adantr 276	. . . . . 6 |- ( ( ph /\ K e. ( M ... N ) ) -> F e. _V )
69		coexg 5202	. . . . . 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 10077	. . . . . 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 5411	. . . . . . . . 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 5408	. . . . . . 7 |- ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> S )
76	75	ffvelcdmda 5685	. . . . . 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 10550	. . . 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 10155	. . . . . . 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 10511	. . . . . . . . . . 11 |- ( K = M -> seq K ( .+ , ( G o. F ) ) = seq M ( .+ , ( G o. F ) ) )
83	82	eqcomd 2199	. . . . . . . . . 10 |- ( K = M -> seq M ( .+ , ( G o. F ) ) = seq K ( .+ , ( G o. F ) ) )
84	83	fveq1d 5548	. . . . . . . . 9 |- ( K = M -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( seq K ( .+ , ( G o. F ) ) ` K ) )
85		f1ocnv 5505	. . . . . . . . . . . . . 14 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
86		f1of 5492	. . . . . . . . . . . . . 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 9638	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
89		eluzfz2 10088	. . . . . . . . . . . . . 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 5686	. . . . . . . . . . . 12 |- ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
92	22, 91	eqeltrid 2280	. . . . . . . . . . 11 |- ( ph -> K e. ( M ... ( N + 1 ) ) )
93	92	elfzelzd 10082	. . . . . . . . . 10 |- ( ph -> K e. ZZ )
94	51, 67, 69	syl2anc 411	. . . . . . . . . 10 |- ( ph -> ( G o. F ) e. _V )
95		seq1g 10524	. . . . . . . . . 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 2248	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
98	97	oveq1d 5925	. . . . . . 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 10087	. . . . . . . . . . 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 2270	. . . . . . . 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 9638	. . . . . . . . . . 11 |- ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
109		fzss1 10119	. . . . . . . . . . 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 10579	. . . . . . . . 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 9334	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( M ... N ) ) -> 1 e. ZZ )
114		elfzuz 10077	. . . . . . . . . . . . . . . . . 18 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ( ZZ>= ` M ) )
115		fzss1 10119	. . . . . . . . . . . . . . . . . 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 3179	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... N ) )
118	25	ffvelcdmda 5685	. . . . . . . . . . . . . . . 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 5571	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
121		breq1 4032	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> ( k < K <-> x < K ) )
122		id 19	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> k = x )
123		oveq1 5917	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> ( k + 1 ) = ( x + 1 ) )
124	121, 122, 123	ifbieq12d 3583	. . . . . . . . . . . . . . . . . 18 |- ( k = x -> if ( k < K , k , ( k + 1 ) ) = if ( x < K , x , ( x + 1 ) ) )
125	124	fveq2d 5550	. . . . . . . . . . . . . . . . 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 3177	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... ( N + 1 ) ) )
128		fzp1elp1 10131	. . . . . . . . . . . . . . . . . . . 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 10082	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
131	93	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. ZZ )
132		zdclt 9384	. . . . . . . . . . . . . . . . . . . 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 3593	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> if ( x < K , x , ( x + 1 ) ) e. ( M ... ( N + 1 ) ) )
135	126, 134	ffvelcdmd 5686	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) e. ( M ... ( N + 1 ) ) )
136	21, 125, 117, 135	fvmptd3 5643	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
137	93	zred 9429	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. RR )
138	137	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. RR )
139		elfzelz 10081	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( K ... N ) -> x e. ZZ )
140	139	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
141	140	zred 9429	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. RR )
142		elfzle1 10083	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( K ... N ) -> K <_ x )
143	142	adantl 277	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K <_ x )
144	138, 141, 143	lensymd 8131	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> -. x < K )
145		iffalse 3565	. . . . . . . . . . . . . . . . . 18 |- ( -. x < K -> if ( x < K , x , ( x + 1 ) ) = ( x + 1 ) )
146	145	fveq2d 5550	. . . . . . . . . . . . . . . . 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 2226	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` ( x + 1 ) ) )
149	148	fveq2d 5550	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
150	120, 149	eqtrd 2226	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
151		fvco3 5620	. . . . . . . . . . . . . . 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 5620	. . . . . . . . . . . . . . 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 2236	. . . . . . . . . . . 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 5202	. . . . . . . . . . . 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 10543	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) )
164		fvco3 5620	. . . . . . . . . . . . 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 5549	. . . . . . . . . . . . . 14 |- ( F ` K ) = ( F ` ( `' F ` ( N + 1 ) ) )
167		f1ocnvfv2 5813	. . . . . . . . . . . . . . 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 2238	. . . . . . . . . . . . 13 |- ( ph -> ( F ` K ) = ( N + 1 ) )
170	169	fveq2d 5550	. . . . . . . . . . . 12 |- ( ph -> ( G ` ( F ` K ) ) = ( G ` ( N + 1 ) ) )
171	165, 170	eqtr2d 2227	. . . . . . . . . . 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 5928	. . . . . . . . 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 2229	. . . . . . . 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 10514	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
177	176	fveq1d 5548	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
178	177	oveq1d 5925	. . . . . . 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 2230	. . . . . 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 10077	. . . . . . . . . . 11 |- ( K e. ( ( M + 1 ) ... N ) -> K e. ( ZZ>= ` ( M + 1 ) ) )
181		eluzp1m1 9606	. . . . . . . . . . 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 9430	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. CC )
184		ax-1cn 7955	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
185		pncan 8215	. . . . . . . . . . . . . . . . . . 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 10081	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ZZ )
188		peano2zm 9345	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ZZ -> ( K - 1 ) e. ZZ )
189	92, 187, 188	3syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( K - 1 ) e. ZZ )
190		elfzuz3 10078	. . . . . . . . . . . . . . . . . . . . 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 9430	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> K e. CC )
193		npcan 8218	. . . . . . . . . . . . . . . . . . . . . 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 5550	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
196	191, 195	eleqtrrd 2273	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
197		eluzp1m1 9606	. . . . . . . . . . . . . . . . . . 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 2271	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. ( ZZ>= ` ( K - 1 ) ) )
200		fzss2 10120	. . . . . . . . . . . . . . . . 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 3179	. . . . . . . . . . . . . . 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 5571	. . . . . . . . . . . . 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 10130	. . . . . . . . . . . . . . . . . . . 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 10081	. . . . . . . . . . . . . . . . . . . 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 3593	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( M ... N ) ) -> if ( x < K , x , ( x + 1 ) ) e. ( M ... ( N + 1 ) ) )
213	206, 212	ffvelcdmd 5686	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) e. ( M ... ( N + 1 ) ) )
214	21, 125, 205, 213	fvmptd3 5643	. . . . . . . . . . . . . . . 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 10147	. . . . . . . . . . . . . . . . . . 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 3562	. . . . . . . . . . . . . . . . 17 |- ( x < K -> if ( x < K , x , ( x + 1 ) ) = x )
221	220	fveq2d 5550	. . . . . . . . . . . . . . . 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 2226	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` x ) )
224	223	fveq2d 5550	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` x ) ) )
225	204, 224	eqtr2d 2227	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
226		peano2uz 9638	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
227		fzss2 10120	. . . . . . . . . . . . . . 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 3179	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
230		fvco3 5620	. . . . . . . . . . . . . 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 2236	. . . . . . . . . . 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 10539	. . . . . . . . 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 10129	. . . . . . . . . . . 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 3179	. . . . . . . . . 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 5928	. . . . . . . 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 10533	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) e. S )
250	74, 92	ffvelcdmd 5686	. . . . . . . . . . . 12 |- ( ph -> ( ( G o. F ) ` K ) e. C )
251	18, 250	sseldd 3180	. . . . . . . . . . 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 3179	. . . . . . . . . . . . 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 10533	. . . . . . . . . . 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 6069	. . . . . . . . 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 5408	. . . . . . . . . . . . . . . 16 |- ( ph -> G : ( M ... ( N + 1 ) ) --> S )
261		fssres 5421	. . . . . . . . . . . . . . . 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 5411	. . . . . . . . . . . . . . 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 5685	. . . . . . . . . . . . 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 10533	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) e. S )
269		elfzuz3 10078	. . . . . . . . . . . 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 10533	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) e. S )
274	260, 90	ffvelcdmd 5686	. . . . . . . . . . 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 6069	. . . . . . . . 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 2236	. . . . . . 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 10535	. . . . . . . 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 5925	. . . . . . 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 10081	. . . . . . . . . . . . . . 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 9430	. . . . . . . . . . . . 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 5550	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
290	270, 289	eleqtrrd 2273	. . . . . . . . . 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 10550	. . . . . . . . 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 10514	. . . . . . . . . . 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 5548	. . . . . . . . . 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 5926	. . . . . . . . 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 2226	. . . . . . . 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 5925	. . . . . . 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 2236	. . . . . 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 2226	. . 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 10527	. . . . 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 9429	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x e. RR )
309	308	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
310	10	zred 9429	. . . . . . . . . . . . . . 15 |- ( ph -> N e. RR )
311	310	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
312		peano2re 8145	. . . . . . . . . . . . . . 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 10084	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x <_ N )
315	314	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
316	311	ltp1d 8939	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
317	309, 311, 313, 315, 316	lelttrd 8134	. . . . . . . . . . . . 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 4057	. . . . . . . . . . 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 2226	. . . . . . . . 9 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` x ) )
323	322	fveq2d 5550	. . . . . . . 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 5686	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... ( N + 1 ) ) )
327	326	elfzelzd 10082	. . . . . . . . . . 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 10096	. . . . . . . . . . 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 8122	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K =/= x )
335		elfzp1 10128	. . . . . . . . . . . . . . . 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 5814	. . . . . . . . . . . . . . 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 2201	. . . . . . . . . . . . . 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 2440	. . . . . . . . . 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 5571	. . . . . . . 8 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
349	323, 348	eqtr2d 2227	. . . . . . 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 2236	. . . . . 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 10539	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
356		fvco3 5620	. . . . . . . 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 2240	. . . . . . . . 9 |- ( ( ph /\ K = ( N + 1 ) ) -> ( `' F ` ( N + 1 ) ) = ( N + 1 ) )
361	360	fveq2d 5550	. . . . . . . 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 2228	. . . . . . 7 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( N + 1 ) ) = ( N + 1 ) )
364	363	fveq2d 5550	. . . . . 6 |- ( ( ph /\ K = ( N + 1 ) ) -> ( G ` ( F ` ( N + 1 ) ) ) = ( G ` ( N + 1 ) ) )
365	358, 364	eqtrd 2226	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( N + 1 ) ) )
366	355, 365	oveq12d 5928	. . . 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 2226	. . 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 10128	. . . . 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 10527	. . 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 2236	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 2164   =/= wne 2364   _Vcvv 2760   C_ wss 3153   ifcif 3557   class class class wbr 4029   |-> cmpt 4090   `'ccnv 4654   |` cres 4657   o. ccom 4659   Fn wfn 5241   -->wf 5242   -1-1-onto->wf1o 5245   ` cfv 5246  (class class class)co 5910   Fincfn 6785   CCcc 7860   RRcr 7861   1c1 7863   + caddc 7865   < clt 8044   <_ cle 8045   - cmin 8180   ZZcz 9307   ZZ>=cuz 9582   ...cfz 10064   seqcseq 10508

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-setind 4565  ax-iinf 4616  ax-cnex 7953  ax-resscn 7954  ax-1cn 7955  ax-1re 7956  ax-icn 7957  ax-addcl 7958  ax-addrcl 7959  ax-mulcl 7960  ax-mulrcl 7961  ax-addcom 7962  ax-mulcom 7963  ax-addass 7964  ax-mulass 7965  ax-distr 7966  ax-i2m1 7967  ax-0lt1 7968  ax-1rid 7969  ax-0id 7970  ax-rnegex 7971  ax-precex 7972  ax-cnre 7973  ax-pre-ltirr 7974  ax-pre-ltwlin 7975  ax-pre-lttrn 7976  ax-pre-apti 7977  ax-pre-ltadd 7978  ax-pre-mulgt0 7979

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 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4322  df-iord 4395  df-on 4397  df-ilim 4398  df-suc 4400  df-iom 4619  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-iota 5207  df-fun 5248  df-fn 5249  df-f 5250  df-f1 5251  df-fo 5252  df-f1o 5253  df-fv 5254  df-riota 5865  df-ov 5913  df-oprab 5914  df-mpo 5915  df-1st 6184  df-2nd 6185  df-recs 6349  df-frec 6435  df-1o 6460  df-er 6578  df-en 6786  df-fin 6788  df-pnf 8046  df-mnf 8047  df-xr 8048  df-ltxr 8049  df-le 8050  df-sub 8182  df-neg 8183  df-reap 8584  df-ap 8591  df-inn 8973  df-n0 9231  df-z 9308  df-uz 9583  df-fz 10065  df-fzo 10199  df-seqfrec 10509

This theorem is referenced by:  seqf1og  10582