Metamath Proof Explorer

Theorem seqf1olem2

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

Ref Expression
Hypotheses 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 seqf1olem2 
|- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( seq M ( .+ , G ) ` ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 seqf1o.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqf1o.2 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
3 seqf1o.3 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
4 seqf1o.4 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 seqf1o.5 
 |-  ( ph -> C C_ S )
6 seqf1olem.5 
 |-  ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
7 seqf1olem.6 
 |-  ( ph -> G : ( M ... ( N + 1 ) ) --> C )
8 seqf1olem.7 
 |-  J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
9 seqf1olem.8 
 |-  K = ( `' F ` ( N + 1 ) )
10 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 ) ) )
11 7 ffnd 
 |-  ( ph -> G Fn ( M ... ( N + 1 ) ) )
12 fzssp1 
 |-  ( M ... N ) C_ ( M ... ( N + 1 ) )
13 fnssres 
 |-  ( ( G Fn ( M ... ( N + 1 ) ) /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) Fn ( M ... N ) )
14 11 12 13 sylancl 
 |-  ( ph -> ( G |` ( M ... N ) ) Fn ( M ... N ) )
15 fzfid 
 |-  ( ph -> ( M ... N ) e. Fin )
16 fnfi 
 |-  ( ( ( G |` ( M ... N ) ) Fn ( M ... N ) /\ ( M ... N ) e. Fin ) -> ( G |` ( M ... N ) ) e. Fin )
17 14 15 16 syl2anc 
 |-  ( ph -> ( G |` ( M ... N ) ) e. Fin )
18 17 elexd 
 |-  ( ph -> ( G |` ( M ... N ) ) e. _V )
19 1 2 3 4 5 6 7 8 9 seqf1olem1 
 |-  ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
20 f1of 
 |-  ( J : ( M ... N ) -1-1-onto-> ( M ... N ) -> J : ( M ... N ) --> ( M ... N ) )
21 19 20 syl 
 |-  ( ph -> J : ( M ... N ) --> ( M ... N ) )
22 fex2 
 |-  ( ( J : ( M ... N ) --> ( M ... N ) /\ ( M ... N ) e. Fin /\ ( M ... N ) e. Fin ) -> J e. _V )
23 21 15 15 22 syl3anc 
 |-  ( ph -> J e. _V )
24 18 23 jca 
 |-  ( ph -> ( ( G |` ( M ... N ) ) e. _V /\ J e. _V ) )
25 fssres 
 |-  ( ( G : ( M ... ( N + 1 ) ) --> C /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) : ( M ... N ) --> C )
26 7 12 25 sylancl 
 |-  ( ph -> ( G |` ( M ... N ) ) : ( M ... N ) --> C )
27 19 26 jca 
 |-  ( ph -> ( J : ( M ... N ) -1-1-onto-> ( M ... N ) /\ ( G |` ( M ... N ) ) : ( M ... N ) --> C ) )
28 f1oeq1 
 |-  ( f = J -> ( f : ( M ... N ) -1-1-onto-> ( M ... N ) <-> J : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
29 feq1 
 |-  ( g = ( G |` ( M ... N ) ) -> ( g : ( M ... N ) --> C <-> ( G |` ( M ... N ) ) : ( M ... N ) --> C ) )
30 28 29 bi2anan9r 
 |-  ( ( 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 ) ) )
31 coeq1 
 |-  ( g = ( G |` ( M ... N ) ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. f ) )
32 coeq2 
 |-  ( f = J -> ( ( G |` ( M ... N ) ) o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
33 31 32 sylan9eq 
 |-  ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( g o. f ) = ( ( G |` ( M ... N ) ) o. J ) )
34 33 seqeq3d 
 |-  ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , ( g o. f ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
35 34 fveq1d 
 |-  ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
36 simpl 
 |-  ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> g = ( G |` ( M ... N ) ) )
37 36 seqeq3d 
 |-  ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> seq M ( .+ , g ) = seq M ( .+ , ( G |` ( M ... N ) ) ) )
38 37 fveq1d 
 |-  ( ( g = ( G |` ( M ... N ) ) /\ f = J ) -> ( seq M ( .+ , g ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
39 35 38 eqeq12d 
 |-  ( ( 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 ) ) )
40 30 39 imbi12d 
 |-  ( ( 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 ) ) ) )
41 40 spc2gv 
 |-  ( ( ( 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 ) ) ) )
42 24 10 27 41 syl3c 
 |-  ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) )
43 fvres 
 |-  ( x e. ( M ... N ) -> ( ( G |` ( M ... N ) ) ` x ) = ( G ` x ) )
44 43 adantl 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` x ) = ( G ` x ) )
45 4 44 seqfveq 
 |-  ( ph -> ( seq M ( .+ , ( G |` ( M ... N ) ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
46 42 45 eqtrd 
 |-  ( ph -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
47 46 oveq1d 
 |-  ( ph -> ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
48 1 adantlr 
 |-  ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
49 3 adantlr 
 |-  ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
50 elfzuz3 
 |-  ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
51 50 adantl 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> N e. ( ZZ>= ` K ) )
52 eluzp1p1 
 |-  ( N e. ( ZZ>= ` K ) -> ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
53 51 52 syl 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
54 elfzuz 
 |-  ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
55 54 adantl 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> K e. ( ZZ>= ` M ) )
56 f1of 
 |-  ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
57 6 56 syl 
 |-  ( ph -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
58 fco 
 |-  ( ( G : ( M ... ( N + 1 ) ) --> C /\ F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) ) -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
59 7 57 58 syl2anc 
 |-  ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
60 59 5 fssd 
 |-  ( ph -> ( G o. F ) : ( M ... ( N + 1 ) ) --> S )
61 60 ffvelcdmda 
 |-  ( ( ph /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
62 61 adantlr 
 |-  ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
63 48 49 53 55 62 seqsplit 
 |-  ( ( 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 ) ) ) )
64 elfzp12 
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )
65 64 biimpa 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ( M ... N ) ) -> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) )
66 4 65 sylan 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) )
67 seqeq1 
 |-  ( K = M -> seq K ( .+ , ( G o. F ) ) = seq M ( .+ , ( G o. F ) ) )
68 67 eqcomd 
 |-  ( K = M -> seq M ( .+ , ( G o. F ) ) = seq K ( .+ , ( G o. F ) ) )
69 68 fveq1d 
 |-  ( K = M -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( seq K ( .+ , ( G o. F ) ) ` K ) )
70 f1ocnv 
 |-  ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
71 f1of 
 |-  ( `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
72 6 70 71 3syl 
 |-  ( ph -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
73 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
74 eluzfz2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
75 4 73 74 3syl 
 |-  ( ph -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
76 72 75 ffvelcdmd 
 |-  ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
77 9 76 eqeltrid 
 |-  ( ph -> K e. ( M ... ( N + 1 ) ) )
78 elfzelz 
 |-  ( K e. ( M ... ( N + 1 ) ) -> K e. ZZ )
79 seq1 
 |-  ( K e. ZZ -> ( seq K ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
80 77 78 79 3syl 
 |-  ( ph -> ( seq K ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
81 69 80 sylan9eqr 
 |-  ( ( ph /\ K = M ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( G o. F ) ` K ) )
82 81 oveq1d 
 |-  ( ( 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 ) ) ) )
83 simpr 
 |-  ( ( ph /\ K = M ) -> K = M )
84 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
85 4 84 syl 
 |-  ( ph -> M e. ( M ... N ) )
86 85 adantr 
 |-  ( ( ph /\ K = M ) -> M e. ( M ... N ) )
87 83 86 eqeltrd 
 |-  ( ( ph /\ K = M ) -> K e. ( M ... N ) )
88 2 adantlr 
 |-  ( ( ( ph /\ K e. ( M ... N ) ) /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
89 5 adantr 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> C C_ S )
90 59 adantr 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> ( G o. F ) : ( M ... ( N + 1 ) ) --> C )
91 77 adantr 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> K e. ( M ... ( N + 1 ) ) )
92 peano2uz 
 |-  ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
93 fzss1 
 |-  ( ( K + 1 ) e. ( ZZ>= ` M ) -> ( ( K + 1 ) ... ( N + 1 ) ) C_ ( M ... ( N + 1 ) ) )
94 55 92 93 3syl 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> ( ( K + 1 ) ... ( N + 1 ) ) C_ ( M ... ( N + 1 ) ) )
95 48 88 49 53 89 90 91 94 seqf1olem2a 
 |-  ( ( 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 ) ) )
96 1zzd 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> 1 e. ZZ )
97 elfzuz 
 |-  ( K e. ( M ... ( N + 1 ) ) -> K e. ( ZZ>= ` M ) )
98 fzss1 
 |-  ( K e. ( ZZ>= ` M ) -> ( K ... N ) C_ ( M ... N ) )
99 77 97 98 3syl 
 |-  ( ph -> ( K ... N ) C_ ( M ... N ) )
100 99 sselda 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> x e. ( M ... N ) )
101 21 ffvelcdmda 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( J ` x ) e. ( M ... N ) )
102 100 101 syldan 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) e. ( M ... N ) )
103 102 fvresd 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
104 breq1 
 |-  ( k = x -> ( k < K <-> x < K ) )
105 id 
 |-  ( k = x -> k = x )
106 oveq1 
 |-  ( k = x -> ( k + 1 ) = ( x + 1 ) )
107 104 105 106 ifbieq12d 
 |-  ( k = x -> if ( k < K , k , ( k + 1 ) ) = if ( x < K , x , ( x + 1 ) ) )
108 107 fveq2d 
 |-  ( k = x -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
109 fvex 
 |-  ( F ` if ( x < K , x , ( x + 1 ) ) ) e. _V
110 108 8 109 fvmpt 
 |-  ( x e. ( M ... N ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
111 100 110 syl 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
112 77 78 syl 
 |-  ( ph -> K e. ZZ )
113 112 zred 
 |-  ( ph -> K e. RR )
114 113 adantr 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> K e. RR )
115 elfzelz 
 |-  ( x e. ( K ... N ) -> x e. ZZ )
116 115 adantl 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> x e. ZZ )
117 116 zred 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> x e. RR )
118 elfzle1 
 |-  ( x e. ( K ... N ) -> K <_ x )
119 118 adantl 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> K <_ x )
120 114 117 119 lensymd 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> -. x < K )
121 iffalse 
 |-  ( -. x < K -> if ( x < K , x , ( x + 1 ) ) = ( x + 1 ) )
122 121 fveq2d 
 |-  ( -. x < K -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` ( x + 1 ) ) )
123 120 122 syl 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` ( x + 1 ) ) )
124 111 123 eqtrd 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( J ` x ) = ( F ` ( x + 1 ) ) )
125 124 fveq2d 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
126 103 125 eqtrd 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
127 fvco3 
 |-  ( ( J : ( M ... N ) --> ( M ... N ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
128 21 127 sylan 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
129 100 128 syldan 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
130 fzp1elp1 
 |-  ( x e. ( M ... N ) -> ( x + 1 ) e. ( M ... ( N + 1 ) ) )
131 100 130 syl 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( x + 1 ) e. ( M ... ( N + 1 ) ) )
132 fvco3 
 |-  ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ ( x + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
133 57 132 sylan 
 |-  ( ( ph /\ ( x + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
134 131 133 syldan 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( ( G o. F ) ` ( x + 1 ) ) = ( G ` ( F ` ( x + 1 ) ) ) )
135 126 129 134 3eqtr4d 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G o. F ) ` ( x + 1 ) ) )
136 135 adantlr 
 |-  ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G o. F ) ` ( x + 1 ) ) )
137 51 96 136 seqshft2 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) )
138 fvco3 
 |-  ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ K e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` K ) = ( G ` ( F ` K ) ) )
139 57 77 138 syl2anc 
 |-  ( ph -> ( ( G o. F ) ` K ) = ( G ` ( F ` K ) ) )
140 9 fveq2i 
 |-  ( F ` K ) = ( F ` ( `' F ` ( N + 1 ) ) )
141 f1ocnvfv2 
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
142 6 75 141 syl2anc 
 |-  ( ph -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
143 140 142 eqtrid 
 |-  ( ph -> ( F ` K ) = ( N + 1 ) )
144 143 fveq2d 
 |-  ( ph -> ( G ` ( F ` K ) ) = ( G ` ( N + 1 ) ) )
145 139 144 eqtr2d 
 |-  ( ph -> ( G ` ( N + 1 ) ) = ( ( G o. F ) ` K ) )
146 145 adantr 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> ( G ` ( N + 1 ) ) = ( ( G o. F ) ` K ) )
147 137 146 oveq12d 
 |-  ( ( 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 ) ) )
148 95 147 eqtr4d 
 |-  ( ( 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 ) ) ) )
149 87 148 syldan 
 |-  ( ( 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 ) ) ) )
150 83 seqeq1d 
 |-  ( ( ph /\ K = M ) -> seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
151 150 fveq1d 
 |-  ( ( ph /\ K = M ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
152 151 oveq1d 
 |-  ( ( 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 ) ) ) )
153 82 149 152 3eqtrd 
 |-  ( ( 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 ) ) ) )
154 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
155 4 154 syl 
 |-  ( ph -> M e. ZZ )
156 elfzuz 
 |-  ( K e. ( ( M + 1 ) ... N ) -> K e. ( ZZ>= ` ( M + 1 ) ) )
157 eluzp1m1 
 |-  ( ( M e. ZZ /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( K - 1 ) e. ( ZZ>= ` M ) )
158 155 156 157 syl2an 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( K - 1 ) e. ( ZZ>= ` M ) )
159 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
160 4 159 syl 
 |-  ( ph -> N e. ZZ )
161 160 zcnd 
 |-  ( ph -> N e. CC )
162 ax-1cn 
 |-  1 e. CC
163 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
164 161 162 163 sylancl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
165 peano2zm 
 |-  ( K e. ZZ -> ( K - 1 ) e. ZZ )
166 77 78 165 3syl 
 |-  ( ph -> ( K - 1 ) e. ZZ )
167 elfzuz3 
 |-  ( K e. ( M ... ( N + 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` K ) )
168 77 167 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` K ) )
169 112 zcnd 
 |-  ( ph -> K e. CC )
170 npcan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
171 169 162 170 sylancl 
 |-  ( ph -> ( ( K - 1 ) + 1 ) = K )
172 171 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
173 168 172 eleqtrrd 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
174 eluzp1m1 
 |-  ( ( ( K - 1 ) e. ZZ /\ ( N + 1 ) e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) ) -> ( ( N + 1 ) - 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
175 166 173 174 syl2anc 
 |-  ( ph -> ( ( N + 1 ) - 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
176 164 175 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( K - 1 ) ) )
177 fzss2 
 |-  ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( M ... ( K - 1 ) ) C_ ( M ... N ) )
178 176 177 syl 
 |-  ( ph -> ( M ... ( K - 1 ) ) C_ ( M ... N ) )
179 178 sselda 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... N ) )
180 179 101 syldan 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) e. ( M ... N ) )
181 180 fvresd 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( G ` ( J ` x ) ) )
182 179 110 syl 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
183 elfzm11 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( x e. ( M ... ( K - 1 ) ) <-> ( x e. ZZ /\ M <_ x /\ x < K ) ) )
184 155 112 183 syl2anc 
 |-  ( ph -> ( x e. ( M ... ( K - 1 ) ) <-> ( x e. ZZ /\ M <_ x /\ x < K ) ) )
185 184 biimpa 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( x e. ZZ /\ M <_ x /\ x < K ) )
186 185 simp3d 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x < K )
187 iftrue 
 |-  ( x < K -> if ( x < K , x , ( x + 1 ) ) = x )
188 187 fveq2d 
 |-  ( x < K -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
189 186 188 syl 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
190 182 189 eqtrd 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( J ` x ) = ( F ` x ) )
191 190 fveq2d 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( J ` x ) ) = ( G ` ( F ` x ) ) )
192 181 191 eqtr2d 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
193 peano2uz 
 |-  ( N e. ( ZZ>= ` ( K - 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
194 fzss2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` ( K - 1 ) ) -> ( M ... ( K - 1 ) ) C_ ( M ... ( N + 1 ) ) )
195 176 193 194 3syl 
 |-  ( ph -> ( M ... ( K - 1 ) ) C_ ( M ... ( N + 1 ) ) )
196 195 sselda 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
197 fvco3 
 |-  ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
198 57 197 sylan 
 |-  ( ( ph /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
199 196 198 syldan 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
200 179 128 syldan 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
201 192 199 200 3eqtr4d 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
202 201 adantlr 
 |-  ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
203 158 202 seqfveq 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) )
204 fzp1ss 
 |-  ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
205 4 154 204 3syl 
 |-  ( ph -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
206 205 sselda 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. ( M ... N ) )
207 206 148 syldan 
 |-  ( ( 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 ) ) ) )
208 203 207 oveq12d 
 |-  ( ( 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 ) ) ) ) )
209 196 61 syldan 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
210 209 adantlr 
 |-  ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
211 1 adantlr 
 |-  ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
212 158 210 211 seqcl 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) e. S )
213 59 77 ffvelcdmd 
 |-  ( ph -> ( ( G o. F ) ` K ) e. C )
214 5 213 sseldd 
 |-  ( ph -> ( ( G o. F ) ` K ) e. S )
215 214 adantr 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( G o. F ) ` K ) e. S )
216 94 sselda 
 |-  ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( ( K + 1 ) ... ( N + 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
217 216 62 syldan 
 |-  ( ( ( ph /\ K e. ( M ... N ) ) /\ x e. ( ( K + 1 ) ... ( N + 1 ) ) ) -> ( ( G o. F ) ` x ) e. S )
218 53 217 48 seqcl 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) e. S )
219 206 218 syldan 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq ( K + 1 ) ( .+ , ( G o. F ) ) ` ( N + 1 ) ) e. S )
220 212 215 219 3jca 
 |-  ( ( 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 ) )
221 3 caovassg 
 |-  ( ( 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 ) ) ) ) )
222 220 221 syldan 
 |-  ( ( 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 ) ) ) ) )
223 7 5 fssd 
 |-  ( ph -> G : ( M ... ( N + 1 ) ) --> S )
224 fssres 
 |-  ( ( G : ( M ... ( N + 1 ) ) --> S /\ ( M ... N ) C_ ( M ... ( N + 1 ) ) ) -> ( G |` ( M ... N ) ) : ( M ... N ) --> S )
225 223 12 224 sylancl 
 |-  ( ph -> ( G |` ( M ... N ) ) : ( M ... N ) --> S )
226 fco 
 |-  ( ( ( G |` ( M ... N ) ) : ( M ... N ) --> S /\ J : ( M ... N ) --> ( M ... N ) ) -> ( ( G |` ( M ... N ) ) o. J ) : ( M ... N ) --> S )
227 225 21 226 syl2anc 
 |-  ( ph -> ( ( G |` ( M ... N ) ) o. J ) : ( M ... N ) --> S )
228 227 ffvelcdmda 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
229 179 228 syldan 
 |-  ( ( ph /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
230 229 adantlr 
 |-  ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
231 158 230 211 seqcl 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` ( K - 1 ) ) e. S )
232 elfzuz3 
 |-  ( K e. ( ( M + 1 ) ... N ) -> N e. ( ZZ>= ` K ) )
233 232 adantl 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> N e. ( ZZ>= ` K ) )
234 100 228 syldan 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
235 234 adantlr 
 |-  ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( K ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
236 233 235 211 seqcl 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) e. S )
237 223 75 ffvelcdmd 
 |-  ( ph -> ( G ` ( N + 1 ) ) e. S )
238 237 adantr 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( G ` ( N + 1 ) ) e. S )
239 231 236 238 3jca 
 |-  ( ( 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 ) )
240 3 caovassg 
 |-  ( ( 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 ) ) ) ) )
241 239 240 syldan 
 |-  ( ( 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 ) ) ) ) )
242 208 222 241 3eqtr4d 
 |-  ( ( 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 ) ) ) )
243 seqm1 
 |-  ( ( 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 ) ) )
244 155 156 243 syl2an 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` K ) = ( ( seq M ( .+ , ( G o. F ) ) ` ( K - 1 ) ) .+ ( ( G o. F ) ` K ) ) )
245 244 oveq1d 
 |-  ( ( 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 ) ) ) )
246 3 adantlr 
 |-  ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
247 elfzelz 
 |-  ( K e. ( ( M + 1 ) ... N ) -> K e. ZZ )
248 247 adantl 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. ZZ )
249 248 zcnd 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> K e. CC )
250 249 162 170 sylancl 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ( K - 1 ) + 1 ) = K )
251 250 fveq2d 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
252 233 251 eleqtrrd 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> N e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
253 228 adantlr 
 |-  ( ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) e. S )
254 211 246 252 158 253 seqsplit 
 |-  ( ( 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 ) ) )
255 250 seqeq1d 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> seq ( ( K - 1 ) + 1 ) ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) = seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) )
256 255 fveq1d 
 |-  ( ( ph /\ K e. ( ( M + 1 ) ... N ) ) -> ( seq ( ( K - 1 ) + 1 ) ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) = ( seq K ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
257 256 oveq2d 
 |-  ( ( 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 ) ) )
258 254 257 eqtrd 
 |-  ( ( 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 ) ) )
259 258 oveq1d 
 |-  ( ( 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 ) ) ) )
260 242 245 259 3eqtr4d 
 |-  ( ( 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 ) ) ) )
261 153 260 jaodan 
 |-  ( ( 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 ) ) ) )
262 66 261 syldan 
 |-  ( ( 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 ) ) ) )
263 63 262 eqtrd 
 |-  ( ( ph /\ K e. ( M ... N ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
264 4 adantr 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> N e. ( ZZ>= ` M ) )
265 seqp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` N ) .+ ( ( G o. F ) ` ( N + 1 ) ) ) )
266 264 265 syl 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( G o. F ) ) ` N ) .+ ( ( G o. F ) ` ( N + 1 ) ) ) )
267 110 adantl 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` if ( x < K , x , ( x + 1 ) ) ) )
268 elfzelz 
 |-  ( x e. ( M ... N ) -> x e. ZZ )
269 268 zred 
 |-  ( x e. ( M ... N ) -> x e. RR )
270 269 adantl 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
271 160 zred 
 |-  ( ph -> N e. RR )
272 271 adantr 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
273 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
274 272 273 syl 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) e. RR )
275 elfzle2 
 |-  ( x e. ( M ... N ) -> x <_ N )
276 275 adantl 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
277 272 ltp1d 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
278 270 272 274 276 277 lelttrd 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
279 278 adantlr 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
280 simplr 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K = ( N + 1 ) )
281 279 280 breqtrrd 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x < K )
282 281 188 syl 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` if ( x < K , x , ( x + 1 ) ) ) = ( F ` x ) )
283 267 282 eqtrd 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( J ` x ) = ( F ` x ) )
284 283 fveq2d 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( J ` x ) ) = ( ( G |` ( M ... N ) ) ` ( F ` x ) ) )
285 269 adantl 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x e. RR )
286 285 281 gtned 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> K =/= x )
287 57 ad2antrr 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
288 fzelp1 
 |-  ( x e. ( M ... N ) -> x e. ( M ... ( N + 1 ) ) )
289 288 adantl 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> x e. ( M ... ( N + 1 ) ) )
290 287 289 ffvelcdmd 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... ( N + 1 ) ) )
291 4 ad2antrr 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> N e. ( ZZ>= ` M ) )
292 elfzp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( F ` x ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) ) )
293 291 292 syl 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) ) )
294 290 293 mpbid 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) e. ( M ... N ) \/ ( F ` x ) = ( N + 1 ) ) )
295 294 ord 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( -. ( F ` x ) e. ( M ... N ) -> ( F ` x ) = ( N + 1 ) ) )
296 6 ad2antrr 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
297 f1ocnvfv 
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( ( F ` x ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = x ) )
298 296 289 297 syl2anc 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = x ) )
299 9 eqeq1i 
 |-  ( K = x <-> ( `' F ` ( N + 1 ) ) = x )
300 298 299 imbitrrdi 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( F ` x ) = ( N + 1 ) -> K = x ) )
301 295 300 syld 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( -. ( F ` x ) e. ( M ... N ) -> K = x ) )
302 301 necon1ad 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( K =/= x -> ( F ` x ) e. ( M ... N ) ) )
303 286 302 mpd 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. ( M ... N ) )
304 303 fvresd 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G |` ( M ... N ) ) ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
305 284 304 eqtr2d 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( G ` ( F ` x ) ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
306 57 288 197 syl2an 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
307 306 adantlr 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
308 128 adantlr 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( ( G |` ( M ... N ) ) o. J ) ` x ) = ( ( G |` ( M ... N ) ) ` ( J ` x ) ) )
309 305 307 308 3eqtr4d 
 |-  ( ( ( ph /\ K = ( N + 1 ) ) /\ x e. ( M ... N ) ) -> ( ( G o. F ) ` x ) = ( ( ( G |` ( M ... N ) ) o. J ) ` x ) )
310 264 309 seqfveq 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` N ) = ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) )
311 fvco3 
 |-  ( ( F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
312 57 75 311 syl2anc 
 |-  ( ph -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
313 312 adantr 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( F ` ( N + 1 ) ) ) )
314 simpr 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> K = ( N + 1 ) )
315 9 314 eqtr3id 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( `' F ` ( N + 1 ) ) = ( N + 1 ) )
316 315 fveq2d 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( F ` ( N + 1 ) ) )
317 142 adantr 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( `' F ` ( N + 1 ) ) ) = ( N + 1 ) )
318 316 317 eqtr3d 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( F ` ( N + 1 ) ) = ( N + 1 ) )
319 318 fveq2d 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( G ` ( F ` ( N + 1 ) ) ) = ( G ` ( N + 1 ) ) )
320 313 319 eqtrd 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( ( G o. F ) ` ( N + 1 ) ) = ( G ` ( N + 1 ) ) )
321 310 320 oveq12d 
 |-  ( ( 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 ) ) ) )
322 266 321 eqtrd 
 |-  ( ( ph /\ K = ( N + 1 ) ) -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
323 elfzp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... ( N + 1 ) ) <-> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) ) )
324 4 323 syl 
 |-  ( ph -> ( K e. ( M ... ( N + 1 ) ) <-> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) ) )
325 77 324 mpbid 
 |-  ( ph -> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) )
326 263 322 325 mpjaodan 
 |-  ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( ( seq M ( .+ , ( ( G |` ( M ... N ) ) o. J ) ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
327 seqp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( seq M ( .+ , G ) ` ( N + 1 ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
328 4 327 syl 
 |-  ( ph -> ( seq M ( .+ , G ) ` ( N + 1 ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` ( N + 1 ) ) ) )
329 47 326 328 3eqtr4d 
 |-  ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( seq M ( .+ , G ) ` ( N + 1 ) ) )