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 ffvelrnda
 |-  ( ( 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 ffvelrnd
 |-  ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnd
 |-  ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnd
 |-  ( 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 ffvelrnd
 |-  ( ( ( 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 syl6ibr
 |-  ( ( ( 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 ) ) )