Theorem seqf1olem2 12841

Description: Lemma for seqf1o 12842. (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 )
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
seqf1olem2	|- ( 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)

Proof of Theorem seqf1olem2

Step	Hyp	Ref	Expression
1		seqf1olem.6	. . . . . . . . . 10 |- ( ph -> G : ( M ... ( N + 1 ) ) --> C )
2		ffn 6045	. . . . . . . . . 10 |- ( G : ( M ... ( N + 1 ) ) --> C -> G Fn ( M ... ( N + 1 ) ) )
3	1, 2	syl 17	. . . . . . . . 9 |- ( ph -> G Fn ( M ... ( N + 1 ) ) )
4		fzssp1 12384	. . . . . . . . 9 |- ( M ... N ) C_ ( M ... ( N + 1 ) )
5		fnssres 6004	. . . . . . . . 9 |- ( ( G Fn ( M ... ( N + 1 ) ) /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) Fn ( M ... N ) )
6	3, 4, 5	sylancl 694	. . . . . . . 8 |- ( ph -> ( G |` ( M ... N ) ) Fn ( M ... N ) )
7		fzfid 12772	. . . . . . . 8 |- ( ph -> ( M ... N ) e. Fin )
8		fnfi 8238	. . . . . . . 8 |- ( ( ( G |` ( M ... N ) ) Fn ( M ... N ) /\ ( M ... N ) e. Fin ) -> ( G |` ( M ... N ) ) e. Fin )
9	6, 7, 8	syl2anc 693	. . . . . . 7 |- ( ph -> ( G |` ( M ... N ) ) e. Fin )
10		elex 3212	. . . . . . 7 |- ( ( G |` ( M ... N ) ) e. Fin -> ( G |` ( M ... N ) ) e. _V )
11	9, 10	syl 17	. . . . . 6 |- ( ph -> ( G |` ( M ... N ) ) e. _V )
12		seqf1o.1	. . . . . . . . 9 |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
13		seqf1o.2	. . . . . . . . 9 |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
14		seqf1o.3	. . . . . . . . 9 |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
15		seqf1o.4	. . . . . . . . 9 |- ( ph -> N e. ( ZZ>= ` M ) )
16		seqf1o.5	. . . . . . . . 9 |- ( ph -> C C_ S )
17		seqf1olem.5	. . . . . . . . 9 |- ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
18		seqf1olem.7	. . . . . . . . 9 |- J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
19		seqf1olem.8	. . . . . . . . 9 |- K = ( `' F ` ( N + 1 ) )
20	12, 13, 14, 15, 16, 17, 1, 18, 19	seqf1olem1 12840	. . . . . . . 8 |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
21		f1of 6137	. . . . . . . 8 |- ( J : ( M ... N ) -1-1-onto-> ( M ... N ) -> J : ( M ... N ) --> ( M ... N ) )
22	20, 21	syl 17	. . . . . . 7 |- ( ph -> J : ( M ... N ) --> ( M ... N ) )
23		fex2 7121	. . . . . . 7 |- ( ( J : ( M ... N ) --> ( M ... N ) /\ ( M ... N ) e. Fin /\ ( M ... N ) e. Fin ) -> J e. _V )
24	22, 7, 7, 23	syl3anc 1326	. . . . . 6 |- ( ph -> J e. _V )
25	11, 24	jca 554	. . . . 5 |- ( ph -> ( ( G |` ( M ... N ) ) e. _V /\ J e. _V ) )
26		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 ) ) )
27		fssres 6070	. . . . . . 7 |- ( ( G : ( M ... ( N + 1 ) ) --> C /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) : ( M ... N ) --> C )
28	1, 4, 27	sylancl 694	. . . . . 6 |- ( ph -> ( G |` ( M ... N ) ) : ( M ... N ) --> C )
29	20, 28	jca 554	. . . . 5 |- ( ph -> ( J : ( M ... N ) -1-1-onto-> ( M ... N ) /\ ( G |` ( M ... N ) ) : ( M ... N ) --> C ) )
30		f1oeq1 6127	. . . . . . . 8 |- ( f = J -> ( f : ( M ... N ) -1-1-onto-> ( M ... N ) <-> J : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
31		feq1 6026	. . . . . . . 8 |- ( g = ( G |` ( M ... N ) ) -> ( g : ( M ... N ) --> C <-> ( G |` ( M ... N ) ) : ( M ... N ) --> C ) )
32	30, 31	bi2anan9r 918	. . . . . . 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 ) ) )
33		coeq1 5279	. . . . . . . . . . 11 |- ( g = ( G |` ( M ... N ) ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. f ) )
34		coeq2 5280	. . . . . . . . . . 11 |- ( f = J -> ( ( G |` ( M ... N ) ) o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
35	33, 34	sylan9eq 2676	. . . . . . . . . 10 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
36	35	seqeq3d 12809	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , ( g o. f ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
37	36	fveq1d 6193	. . . . . . . 8 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
38		simpl 473	. . . . . . . . . 10 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> g = ( G |` ( M ... N ) ) )
39	38	seqeq3d 12809	. . . . . . . . 9 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , g ) = seq M ( .+ , ( G |` ( M ... N ) ) ) )
40	39	fveq1d 6193	. . . . . . . 8 |- ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , g ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
41	37, 40	eqeq12d 2637	. . . . . . 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 ) ) )
42	32, 41	imbi12d 334	. . . . . 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 ) ) ) )
43	42	spc2gv 3296	. . . . 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 ) ) ) )
44	25, 26, 29, 43	syl3c 66	. . . 4 |- ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
45		fvres 6207	. . . . . 6 |- ( x e. ( M ... N ) -> ( ( G |` ( M ... N ) ) ` x ) = ( G ` x ) )
46	45	adantl 482	. . . . 5 |- ( ( ph /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` x ) = ( G ` x ) )
47	15, 46	seqfveq 12825	. . . 4 |- ( ph -> ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
48	44, 47	eqtrd 2656	. . 3 |- ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
49	48	oveq1d 6665	. 2 |- ( ph -> ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
50	12	adantlr 751	. . . . 5 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
51	14	adantlr 751	. . . . 5 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
52		elfzuz3 12339	. . . . . . 7 |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
53	52	adantl 482	. . . . . 6 |- ( ( ph /\ K e. ( M ... N ) ) -> N e. ( ZZ>= ` K ) )
54		eluzp1p1 11713	. . . . . 6 |- ( N e. ( ZZ>= ` K ) -> ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
55	53, 54	syl 17	. . . . 5 |- ( ( ph /\ K e. ( M ... N ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
56		elfzuz 12338	. . . . . 6 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
57	56	adantl 482	. . . . 5 |- ( ( ph /\ K e. ( M ... N ) ) -> K e. ( ZZ>= ` M ) )
58		f1of 6137	. . . . . . . . . 10 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
59	17, 58	syl 17	. . . . . . . . 9 |- ( ph -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
60		fco 6058	. . . . . . . . 9 |- ( ( G : ( M ... ( N + 1 ) ) --> C /\ F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) ) -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
61	1, 59, 60	syl2anc 693	. . . . . . . 8 |- ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
62	61, 16	fssd 6057	. . . . . . 7 |- ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> S )
63	62	ffvelrnda 6359	. . . . . 6 |- ( ( ph /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
64	63	adantlr 751	. . . . 5 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
65	50, 51, 55, 57, 64	seqsplit 12834	. . . 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 ) ) ) )
66		elfzp12 12419	. . . . . . 7 |- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )
67	66	biimpa 501	. . . . . 6 |- ( ( N e. ( ZZ>= ` M ) /\ K e. ( M ... N ) ) -> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) )
68	15, 67	sylan 488	. . . . 5 |- ( ( ph /\ K e. ( M ... N ) ) -> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) )
69		seqeq1 12804	. . . . . . . . . . 11 |- ( K = M -> seq K ( .+ , ( G o. F ) ) = seq M ( .+ , ( G o. F ) ) )
70	69	eqcomd 2628	. . . . . . . . . 10 |- ( K = M -> seq M ( .+ , ( G o. F ) ) = seq K ( .+ , ( G o. F ) ) )
71	70	fveq1d 6193	. . . . . . . . 9 |- ( K = M -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( seq K ( .+ , ( G o. F ) ) ` K ) )
72		f1ocnv 6149	. . . . . . . . . . . . 13 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
73		f1of 6137	. . . . . . . . . . . . 13 |- ( `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
74	17, 72, 73	3syl 18	. . . . . . . . . . . 12 |- ( ph -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
75		peano2uz 11741	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
76		eluzfz2 12349	. . . . . . . . . . . . 13 |- ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
77	15, 75, 76	3syl 18	. . . . . . . . . . . 12 |- ( ph -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
78	74, 77	ffvelrnd 6360	. . . . . . . . . . 11 |- ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
79	19, 78	syl5eqel 2705	. . . . . . . . . 10 |- ( ph -> K e. ( M ... ( N + 1 ) ) )
80		elfzelz 12342	. . . . . . . . . 10 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ZZ )
81		seq1 12814	. . . . . . . . . 10 |- ( K e. ZZ -> ( seq K ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
82	79, 80, 81	3syl 18	. . . . . . . . 9 |- ( ph -> ( seq K ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
83	71, 82	sylan9eqr 2678	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
84	83	oveq1d 6665	. . . . . . 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 ) ) ) )
85		simpr 477	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> K = M )
86		eluzfz1 12348	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
87	15, 86	syl 17	. . . . . . . . . 10 |- ( ph -> M e. ( M ... N ) )
88	87	adantr 481	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> M e. ( M ... N ) )
89	85, 88	eqeltrd 2701	. . . . . . . 8 |- ( ( ph /\ K = M ) -> K e. ( M ... N ) )
90	13	adantlr 751	. . . . . . . . . 10 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
91	16	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> C C_ S )
92	61	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
93	79	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> K e. ( M ... ( N + 1 ) ) )
94		peano2uz 11741	. . . . . . . . . . 11 |- ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
95		fzss1 12380	. . . . . . . . . . 11 |- ( ( K + 1 ) e. ( ZZ>= ` M ) -> ( ( K + 1 ) ... ( N + 1 ) ) C_ ( M ... ( N + 1 ) ) )
96	57, 94, 95	3syl 18	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( ( K + 1 ) ... ( N + 1 ) ) C_ ( M ... ( N + 1 ) ) )
97	50, 90, 51, 55, 91, 92, 93, 96	seqf1olem2a 12839	. . . . . . . . 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 ) ) )
98		1zzd 11408	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( M ... N ) ) -> 1 e. ZZ )
99		elfzuz 12338	. . . . . . . . . . . . . . . . . 18 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ( ZZ>= ` M ) )
100		fzss1 12380	. . . . . . . . . . . . . . . . . 18 |- ( K e. ( ZZ>= ` M ) -> ( K ... N ) C_ ( M ... N ) )
101	79, 99, 100	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( K ... N ) C_ ( M ... N ) )
102	101	sselda 3603	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... N ) )
103	22	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( M ... N ) ) -> ( J ` x ) e. ( M ... N ) )
104	102, 103	syldan 487	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) e. ( M ... N ) )
105		fvres 6207	. . . . . . . . . . . . . . 15 |- ( ( J ` x ) e. ( M ... N ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
106	104, 105	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
107		breq1 4656	. . . . . . . . . . . . . . . . . . . 20 |- ( k = x -> ( k < K <-> x < K ) )
108		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( k = x -> k = x )
109		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 |- ( k = x -> ( k + 1 ) = ( x + 1 ) )
110	107, 108, 109	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . 19 |- ( k = x -> if ( k < K , k , ( k + 1 ) ) = if ( x < K , x , ( x + 1 ) ) )
111	110	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( k = x -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
112		fvex 6201	. . . . . . . . . . . . . . . . . 18 |- ( F ` if ( x < K , x , ( x + 1 ) ) ) e. _V
113	111, 18, 112	fvmpt 6282	. . . . . . . . . . . . . . . . 17 |- ( x e. ( M ... N ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
114	102, 113	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
115		elfzle1 12344	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( K ... N ) -> K <_ x )
116	115	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> K <_ x )
117	79, 80	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> K e. ZZ )
118	117	zred 11482	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> K e. RR )
119	118	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> K e. RR )
120		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( K ... N ) -> x e. ZZ )
121	120	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
122	121	zred 11482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( K ... N ) ) -> x e. RR )
123	119, 122	lenltd 10183	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( K ... N ) ) -> ( K <_ x <-> -. x < K ) )
124	116, 123	mpbid 222	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( K ... N ) ) -> -. x < K )
125		iffalse 4095	. . . . . . . . . . . . . . . . . 18 |- ( -. x < K -> if ( x < K , x , ( x + 1 ) ) = ( x + 1 ) )
126	125	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( -. x < K -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` ( x + 1 ) ) )
127	124, 126	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( K ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` ( x + 1 ) ) )
128	114, 127	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` ( x + 1 ) ) )
129	128	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
130	106, 129	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
131		fvco3 6275	. . . . . . . . . . . . . . 15 |- ( ( J : ( M ... N ) --> ( M ... N ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
132	22, 131	sylan 488	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
133	102, 132	syldan 487	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
134		fzp1elp1 12394	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> ( x + 1 ) e. ( M ... ( N + 1 ) ) )
135	102, 134	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( K ... N ) ) -> ( x + 1 ) e. ( M ... ( N + 1 ) ) )
136		fvco3 6275	. . . . . . . . . . . . . . 15 |- ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ ( x + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
137	59, 136	sylan 488	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
138	135, 137	syldan 487	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
139	130, 133, 138	3eqtr4d 2666	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G o. F ) ` ( x + 1 ) ) )
140	139	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G o. F ) ` ( x + 1 ) ) )
141	53, 98, 140	seqshft2 12827	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) )
142		fvco3 6275	. . . . . . . . . . . . 13 |- ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ K e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` K ) = ( G ` ( F ` K ) ) )
143	59, 79, 142	syl2anc 693	. . . . . . . . . . . 12 |- ( ph -> ( ( G o. F ) ` K ) = ( G ` ( F ` K ) ) )
144	19	fveq2i 6194	. . . . . . . . . . . . . 14 |- ( F ` K ) = ( F ` ( `' F ` ( N + 1 ) ) )
145		f1ocnvfv2 6533	. . . . . . . . . . . . . . 15 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
146	17, 77, 145	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
147	144, 146	syl5eq 2668	. . . . . . . . . . . . 13 |- ( ph -> ( F ` K ) = ( N + 1 ) )
148	147	fveq2d 6195	. . . . . . . . . . . 12 |- ( ph -> ( G ` ( F ` K ) ) = ( G ` ( N + 1 ) ) )
149	143, 148	eqtr2d 2657	. . . . . . . . . . 11 |- ( ph -> ( G ` ( N + 1 ) ) = ( ( G o. F ) ` K ) )
150	149	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ K e. ( M ... N ) ) -> ( G ` ( N + 1 ) ) = ( ( G o. F ) ` K ) )
151	141, 150	oveq12d 6668	. . . . . . . . 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 ) ) )
152	97, 151	eqtr4d 2659	. . . . . . . 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 ) ) ) )
153	89, 152	syldan 487	. . . . . . 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 ) ) ) )
154	85	seqeq1d 12807	. . . . . . . . 9 |- ( ( ph /\ K = M ) -> seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
155	154	fveq1d 6193	. . . . . . . 8 |- ( ( ph /\ K = M ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
156	155	oveq1d 6665	. . . . . . 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 ) ) ) )
157	84, 153, 156	3eqtrd 2660	. . . . . 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 ) ) ) )
158		eluzel2 11692	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
159	15, 158	syl 17	. . . . . . . . . . 11 |- ( ph -> M e. ZZ )
160		elfzuz 12338	. . . . . . . . . . 11 |- ( K e. ( ( M + 1 ) ... N ) -> K e. ( ZZ>= ` ( M + 1 ) ) )
161		eluzp1m1 11711	. . . . . . . . . . 11 |- ( ( M e. ZZ /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( K - 1 ) e. ( ZZ>= ` M ) )
162	159, 160, 161	syl2an 494	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( K - 1 ) e. ( ZZ>= ` M ) )
163		eluzelz 11697	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
164	15, 163	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> N e. ZZ )
165	164	zcnd 11483	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. CC )
166		ax-1cn 9994	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
167		pncan 10287	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
168	165, 166, 167	sylancl 694	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
169		peano2zm 11420	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. ZZ -> ( K - 1 ) e. ZZ )
170	79, 80, 169	3syl 18	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( K - 1 ) e. ZZ )
171		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . 21 |- ( K e. ( M ... ( N + 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` K ) )
172	79, 171	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` K ) )
173	117	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> K e. CC )
174		npcan 10290	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
175	173, 166, 174	sylancl 694	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( K - 1 ) + 1 ) = K )
176	175	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
177	172, 176	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
178		eluzp1m1 11711	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( K - 1 ) e. ZZ /\ ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) ) -> ( ( N + 1 ) - 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
179	170, 177, 178	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( N + 1 ) - 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
180	168, 179	eqeltrrd 2702	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. ( ZZ>= ` ( K - 1 ) ) )
181		fzss2 12381	. . . . . . . . . . . . . . . . 17 |- ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( M ... ( K - 1 ) ) C_ ( M ... N ) )
182	180, 181	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( M ... ( K - 1 ) ) C_ ( M ... N ) )
183	182	sselda 3603	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... N ) )
184	183, 103	syldan 487	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) e. ( M ... N ) )
185	184, 105	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
186	183, 113	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
187		elfzm11 12411	. . . . . . . . . . . . . . . . . . 19 |- ( ( M e. ZZ /\ K e. ZZ ) -> ( x e. ( M ... ( K - 1 ) ) <-> ( x e. ZZ /\ M <_ x /\ x < K ) ) )
188	159, 117, 187	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( x e. ( M ... ( K - 1 ) ) <-> ( x e. ZZ /\ M <_ x /\ x < K ) ) )
189	188	biimpa 501	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( x e. ZZ /\ M <_ x /\ x < K ) )
190	189	simp3d 1075	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x < K )
191		iftrue 4092	. . . . . . . . . . . . . . . . 17 |- ( x < K -> if ( x < K , x , ( x + 1 ) ) = x )
192	191	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( x < K -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
193	190, 192	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
194	186, 193	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` x ) )
195	194	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` x ) ) )
196	185, 195	eqtr2d 2657	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
197		peano2uz 11741	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
198		fzss2 12381	. . . . . . . . . . . . . . 15 |- ( ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) -> ( M ... ( K - 1 ) ) C_ ( M ... ( N + 1 ) ) )
199	180, 197, 198	3syl 18	. . . . . . . . . . . . . 14 |- ( ph -> ( M ... ( K - 1 ) ) C_ ( M ... ( N + 1 ) ) )
200	199	sselda 3603	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
201		fvco3 6275	. . . . . . . . . . . . . 14 |- ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
202	59, 201	sylan 488	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
203	200, 202	syldan 487	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
204	183, 132	syldan 487	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
205	196, 203, 204	3eqtr4d 2666	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
206	205	adantlr 751	. . . . . . . . . 10 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
207	162, 206	seqfveq 12825	. . . . . . . . 9 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) )
208		fzp1ss 12392	. . . . . . . . . . . 12 |- ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
209	15, 158, 208	3syl 18	. . . . . . . . . . 11 |- ( ph -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
210	209	sselda 3603	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. ( M ... N ) )
211	210, 152	syldan 487	. . . . . . . . 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 ) ) ) )
212	207, 211	oveq12d 6668	. . . . . . . 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 ) ) ) ) )
213	200, 63	syldan 487	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
214	213	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
215	12	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
216	162, 214, 215	seqcl 12821	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) e. S )
217	61, 79	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ph -> ( ( G o. F ) ` K ) e. C )
218	16, 217	sseldd 3604	. . . . . . . . . . 11 |- ( ph -> ( ( G o. F ) ` K ) e. S )
219	218	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( G o. F ) ` K ) e. S )
220	96	sselda 3603	. . . . . . . . . . . . 13 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( ( K + 1 ) ... ( N + 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
221	220, 64	syldan 487	. . . . . . . . . . . 12 |- ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( ( K + 1 ) ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
222	55, 221, 50	seqcl 12821	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) e. S )
223	210, 222	syldan 487	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) e. S )
224	216, 219, 223	3jca 1242	. . . . . . . . 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 ) )
225	14	caovassg 6832	. . . . . . . . 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 ) ) ) ) )
226	224, 225	syldan 487	. . . . . . . 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 ) ) ) ) )
227	1, 16	fssd 6057	. . . . . . . . . . . . . . . 16 |- ( ph -> G : ( M ... ( N + 1 ) ) --> S )
228		fssres 6070	. . . . . . . . . . . . . . . 16 |- ( ( G : ( M ... ( N + 1 ) ) --> S /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) : ( M ... N ) --> S )
229	227, 4, 228	sylancl 694	. . . . . . . . . . . . . . 15 |- ( ph -> ( G |` ( M ... N ) ) : ( M ... N ) --> S )
230		fco 6058	. . . . . . . . . . . . . . 15 |- ( ( ( G |` ( M ... N ) ) : ( M ... N ) --> S /\ J : ( M ... N ) --> ( M ... N ) ) -> ( ( G |` ( M ... N ) ) o. J ) : ( M ... N ) --> S )
231	229, 22, 230	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G |` ( M ... N ) ) o. J ) : ( M ... N ) --> S )
232	231	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
233	183, 232	syldan 487	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
234	233	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
235	162, 234, 215	seqcl 12821	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) e. S )
236		elfzuz3 12339	. . . . . . . . . . . 12 |- ( K e. ( ( M + 1 ) ... N ) -> N e. ( ZZ>= ` K ) )
237	236	adantl 482	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> N e. ( ZZ>= ` K ) )
238	102, 232	syldan 487	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
239	238	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
240	237, 239, 215	seqcl 12821	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) e. S )
241	227, 77	ffvelrnd 6360	. . . . . . . . . . 11 |- ( ph -> ( G ` ( N + 1 ) ) e. S )
242	241	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( G ` ( N + 1 ) ) e. S )
243	235, 240, 242	3jca 1242	. . . . . . . . 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 ) )
244	14	caovassg 6832	. . . . . . . . 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 ) ) ) ) )
245	243, 244	syldan 487	. . . . . . . 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 ) ) ) ) )
246	212, 226, 245	3eqtr4d 2666	. . . . . . 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 ) ) ) )
247		seqm1 12818	. . . . . . . . 9 |- ( ( M e. ZZ /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( G o. F ) ` K ) ) )
248	159, 160, 247	syl2an 494	. . . . . . . 8 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( G o. F ) ` K ) ) )
249	248	oveq1d 6665	. . . . . . 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 ) ) ) )
250	14	adantlr 751	. . . . . . . . . 10 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
251		elfzelz 12342	. . . . . . . . . . . . . . 15 |- ( K e. ( ( M + 1 ) ... N ) -> K e. ZZ )
252	251	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. ZZ )
253	252	zcnd 11483	. . . . . . . . . . . . 13 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. CC )
254	253, 166, 174	sylancl 694	. . . . . . . . . . . 12 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( K - 1 ) + 1 ) = K )
255	254	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
256	237, 255	eleqtrrd 2704	. . . . . . . . . 10 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> N e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
257	232	adantlr 751	. . . . . . . . . 10 |- ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
258	215, 250, 256, 162, 257	seqsplit 12834	. . . . . . . . 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 ) ) )
259	254	seqeq1d 12807	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> seq ( ( K - 1 ) + 1 ) ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
260	259	fveq1d 6193	. . . . . . . . . 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 ) )
261	260	oveq2d 6666	. . . . . . . . 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 ) ) )
262	258, 261	eqtrd 2656	. . . . . . . 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 ) ) )
263	262	oveq1d 6665	. . . . . . 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 ) ) ) )
264	246, 249, 263	3eqtr4d 2666	. . . . . 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 ) ) ) )
265	157, 264	jaodan 826	. . . . 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 ) ) ) )
266	68, 265	syldan 487	. . . 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 ) ) ) )
267	65, 266	eqtrd 2656	. . 3 |- ( ( ph /\ K e. ( M ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
268	15	adantr 481	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> N e. ( ZZ>= ` M ) )
269		seqp1 12816	. . . . 5 |- ( N e. ( ZZ>= ` M ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` N ) .+ ( ( G o. F ) ` ( N + 1 ) ) ) )
270	268, 269	syl 17	. . . 4 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` N ) .+ ( ( G o. F ) ` ( N + 1 ) ) ) )
271	113	adantl 482	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
272		elfzelz 12342	. . . . . . . . . . . . . . . 16 |- ( x e. ( M ... N ) -> x e. ZZ )
273	272	zred 11482	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x e. RR )
274	273	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
275	164	zred 11482	. . . . . . . . . . . . . . 15 |- ( ph -> N e. RR )
276	275	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
277		peano2re 10209	. . . . . . . . . . . . . . 15 |- ( N e. RR -> ( N + 1 ) e. RR )
278	276, 277	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) e. RR )
279		elfzle2 12345	. . . . . . . . . . . . . . 15 |- ( x e. ( M ... N ) -> x <_ N )
280	279	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
281	276	ltp1d 10954	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
282	274, 276, 278, 280, 281	lelttrd 10195	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
283	282	adantlr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
284		simplr 792	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K = ( N + 1 ) )
285	283, 284	breqtrrd 4681	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x < K )
286	285, 192	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
287	271, 286	eqtrd 2656	. . . . . . . . 9 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` x ) )
288	287	fveq2d 6195	. . . . . . . 8 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( ( G |` ( M ... N ) ) ` ( F ` x ) ) )
289	273	adantl 482	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x e. RR )
290	289, 285	gtned 10172	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K =/= x )
291	59	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
292		fzelp1 12393	. . . . . . . . . . . . . . . 16 |- ( x e. ( M ... N ) -> x e. ( M ... ( N + 1 ) ) )
293	292	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x e. ( M ... ( N + 1 ) ) )
294	291, 293	ffvelrnd 6360	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... ( N + 1 ) ) )
295	15	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> N e. ( ZZ>= ` M ) )
296		elfzp1 12391	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` M ) -> ( ( F ` x ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) ) )
297	295, 296	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) ) )
298	294, 297	mpbid 222	. . . . . . . . . . . . 13 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) )
299	298	ord 392	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( -. ( F ` x ) e. ( M ... N ) -> ( F ` x ) = ( N + 1 ) ) )
300	17	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
301		f1ocnvfv 6534	. . . . . . . . . . . . . 14 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( F ` x ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = x ) )
302	300, 293, 301	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = x ) )
303	19	eqeq1i 2627	. . . . . . . . . . . . 13 |- ( K = x <-> ( `' F ` ( N + 1 ) ) = x )
304	302, 303	syl6ibr 242	. . . . . . . . . . . 12 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) = ( N + 1 ) -> K = x ) )
305	299, 304	syld 47	. . . . . . . . . . 11 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( -. ( F ` x ) e. ( M ... N ) -> K = x ) )
306	305	necon1ad 2811	. . . . . . . . . 10 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( K =/= x -> ( F ` x ) e. ( M ... N ) ) )
307	290, 306	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... N ) )
308		fvres 6207	. . . . . . . . 9 |- ( ( F ` x ) e. ( M ... N ) -> ( ( G |` ( M ... N ) ) ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
309	307, 308	syl 17	. . . . . . . 8 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
310	288, 309	eqtr2d 2657	. . . . . . 7 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
311	59, 292, 201	syl2an 494	. . . . . . . 8 |- ( ( ph /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
312	311	adantlr 751	. . . . . . 7 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
313	132	adantlr 751	. . . . . . 7 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
314	310, 312, 313	3eqtr4d 2666	. . . . . 6 |- ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
315	268, 314	seqfveq 12825	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
316		fvco3 6275	. . . . . . . 8 |- ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
317	59, 77, 316	syl2anc 693	. . . . . . 7 |- ( ph -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
318	317	adantr 481	. . . . . 6 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
319		simpr 477	. . . . . . . . . 10 |- ( ( ph /\ K = ( N + 1 ) ) -> K = ( N + 1 ) )
320	19, 319	syl5eqr 2670	. . . . . . . . 9 |- ( ( ph /\ K = ( N + 1 ) ) -> ( `' F ` ( N + 1 ) ) = ( N + 1 ) )
321	320	fveq2d 6195	. . . . . . . 8 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( F ` ( N + 1 ) ) )
322	146	adantr 481	. . . . . . . 8 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
323	321, 322	eqtr3d 2658	. . . . . . 7 |- ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( N + 1 ) ) = ( N + 1 ) )
324	323	fveq2d 6195	. . . . . 6 |- ( ( ph /\ K = ( N + 1 ) ) -> ( G ` ( F ` ( N + 1 ) ) ) = ( G ` ( N + 1 ) ) )
325	318, 324	eqtrd 2656	. . . . 5 |- ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( N + 1 ) ) )
326	315, 325	oveq12d 6668	. . . 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 ) ) ) )
327	270, 326	eqtrd 2656	. . 3 |- ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
328		elfzp1 12391	. . . . 5 |- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... ( N + 1 ) ) <-> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) ) )
329	15, 328	syl 17	. . . 4 |- ( ph -> ( K e. ( M ... ( N + 1 ) ) <-> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) ) )
330	79, 329	mpbid 222	. . 3 |- ( ph -> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) )
331	267, 327, 330	mpjaodan 827	. 2 |- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
332		seqp1 12816	. . 3 |- ( N e. ( ZZ>= ` M ) -> ( seq M ( .+ , G ) ` ( N + 1 ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
333	15, 332	syl 17	. 2 |- ( ph -> ( seq M ( .+ , G ) ` ( N + 1 ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
334	49, 331, 333	3eqtr4d 2666	1 |- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( seq M ( .+ , G ) ` ( N + 1 ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   e. wcel 1990   =/= wne 2794   _Vcvv 3200   C_ wss 3574   ifcif 4086   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   |` cres 5116   o. ccom 5118   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   Fincfn 7955   CCcc 9934   RRcr 9935   1c1 9937   + caddc 9939   < clt 10074   <_ cle 10075   - cmin 10266   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   seqcseq 12801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802

This theorem is referenced by:  seqf1o  12842