MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqf1olem2 Unicode version

Theorem seqf1olem2 11086
Description: Lemma for seqf1o 11087. (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
StepHypRef Expression
1 seqf1olem.6 . . . . . . . . . 10  |-  ( ph  ->  G : ( M ... ( N  + 
1 ) ) --> C )
2 ffn 5389 . . . . . . . . . 10  |-  ( G : ( M ... ( N  +  1
) ) --> C  ->  G  Fn  ( M ... ( N  +  1 ) ) )
31, 2syl 15 . . . . . . . . 9  |-  ( ph  ->  G  Fn  ( M ... ( N  + 
1 ) ) )
4 fzssp1 10834 . . . . . . . . 9  |-  ( M ... N )  C_  ( M ... ( N  +  1 ) )
5 fnssres 5357 . . . . . . . . 9  |-  ( ( G  Fn  ( M ... ( N  + 
1 ) )  /\  ( M ... N ) 
C_  ( M ... ( N  +  1
) ) )  -> 
( G  |`  ( M ... N ) )  Fn  ( M ... N ) )
63, 4, 5sylancl 643 . . . . . . . 8  |-  ( ph  ->  ( G  |`  ( M ... N ) )  Fn  ( M ... N ) )
7 fzfid 11035 . . . . . . . 8  |-  ( ph  ->  ( M ... N
)  e.  Fin )
8 fnfi 7134 . . . . . . . 8  |-  ( ( ( G  |`  ( M ... N ) )  Fn  ( M ... N )  /\  ( M ... N )  e. 
Fin )  ->  ( G  |`  ( M ... N ) )  e. 
Fin )
96, 7, 8syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( G  |`  ( M ... N ) )  e.  Fin )
10 elex 2796 . . . . . . 7  |-  ( ( G  |`  ( M ... N ) )  e. 
Fin  ->  ( G  |`  ( M ... N ) )  e.  _V )
119, 10syl 15 . . . . . 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
) )
2012, 13, 14, 15, 16, 17, 1, 18, 19seqf1olem1 11085 . . . . . . . 8  |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )
21 f1of 5472 . . . . . . . 8  |-  ( J : ( M ... N ) -1-1-onto-> ( M ... N
)  ->  J :
( M ... N
) --> ( M ... N ) )
2220, 21syl 15 . . . . . . 7  |-  ( ph  ->  J : ( M ... N ) --> ( M ... N ) )
23 fex2 5401 . . . . . . 7  |-  ( ( J : ( M ... N ) --> ( M ... N )  /\  ( M ... N )  e.  Fin  /\  ( M ... N
)  e.  Fin )  ->  J  e.  _V )
2422, 7, 7, 23syl3anc 1182 . . . . . 6  |-  ( ph  ->  J  e.  _V )
2511, 24jca 518 . . . . 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 5408 . . . . . . 7  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> C  /\  ( M ... N )  C_  ( M ... ( N  + 
1 ) ) )  ->  ( G  |`  ( M ... N ) ) : ( M ... N ) --> C )
281, 4, 27sylancl 643 . . . . . 6  |-  ( ph  ->  ( G  |`  ( M ... N ) ) : ( M ... N ) --> C )
2920, 28jca 518 . . . . 5  |-  ( ph  ->  ( J : ( M ... N ) -1-1-onto-> ( M ... N )  /\  ( G  |`  ( M ... N ) ) : ( M ... N ) --> C ) )
30 f1oeq1 5463 . . . . . . . 8  |-  ( f  =  J  ->  (
f : ( M ... N ) -1-1-onto-> ( M ... N )  <->  J :
( M ... N
)
-1-1-onto-> ( M ... N ) ) )
31 feq1 5375 . . . . . . . 8  |-  ( g  =  ( G  |`  ( M ... N ) )  ->  ( g : ( M ... N ) --> C  <->  ( G  |`  ( M ... N
) ) : ( M ... N ) --> C ) )
3230, 31bi2anan9r 844 . . . . . . 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 4841 . . . . . . . . . . 11  |-  ( g  =  ( G  |`  ( M ... N ) )  ->  ( g  o.  f )  =  ( ( G  |`  ( M ... N ) )  o.  f ) )
34 coeq2 4842 . . . . . . . . . . 11  |-  ( f  =  J  ->  (
( G  |`  ( M ... N ) )  o.  f )  =  ( ( G  |`  ( M ... N ) )  o.  J ) )
3533, 34sylan9eq 2335 . . . . . . . . . 10  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  (
g  o.  f )  =  ( ( G  |`  ( M ... N
) )  o.  J
) )
3635seqeq3d 11054 . . . . . . . . 9  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  seq  M (  .+  ,  ( g  o.  f ) )  =  seq  M
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) )
3736fveq1d 5527 . . . . . . . 8  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  (  seq  M (  .+  , 
( g  o.  f
) ) `  N
)  =  (  seq 
M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N ) )
38 simpl 443 . . . . . . . . . 10  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  g  =  ( G  |`  ( M ... N ) ) )
3938seqeq3d 11054 . . . . . . . . 9  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  seq  M (  .+  ,  g )  =  seq  M
(  .+  ,  ( G  |`  ( M ... N ) ) ) )
4039fveq1d 5527 . . . . . . . 8  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  (  seq  M (  .+  , 
g ) `  N
)  =  (  seq 
M (  .+  , 
( G  |`  ( M ... N ) ) ) `  N ) )
4137, 40eqeq12d 2297 . . . . . . 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 ) ) )
4232, 41imbi12d 311 . . . . . 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 ) ) ) )
4342spc2gv 2871 . . . . 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 ) ) ) )
4425, 26, 29, 43syl3c 57 . . . 4  |-  ( ph  ->  (  seq  M ( 
.+  ,  ( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  =  (  seq  M (  .+  ,  ( G  |`  ( M ... N ) ) ) `  N
) )
45 fvres 5542 . . . . . 6  |-  ( x  e.  ( M ... N )  ->  (
( G  |`  ( M ... N ) ) `
 x )  =  ( G `  x
) )
4645adantl 452 . . . . 5  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( ( G  |`  ( M ... N ) ) `  x )  =  ( G `  x ) )
4715, 46seqfveq 11070 . . . 4  |-  ( ph  ->  (  seq  M ( 
.+  ,  ( G  |`  ( M ... N
) ) ) `  N )  =  (  seq  M (  .+  ,  G ) `  N
) )
4844, 47eqtrd 2315 . . 3  |-  ( ph  ->  (  seq  M ( 
.+  ,  ( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  =  (  seq  M (  .+  ,  G ) `  N
) )
4948oveq1d 5873 . 2  |-  ( ph  ->  ( (  seq  M
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) `
 N )  .+  ( G `  ( N  +  1 ) ) )  =  ( (  seq  M (  .+  ,  G ) `  N
)  .+  ( G `  ( N  +  1 ) ) ) )
5012adantlr 695 . . . . 5  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  .+  y )  e.  S
)
5114adantlr 695 . . . . 5  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  (
x  e.  S  /\  y  e.  S  /\  z  e.  S )
)  ->  ( (
x  .+  y )  .+  z )  =  ( x  .+  ( y 
.+  z ) ) )
52 elfzuz3 10795 . . . . . . 7  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
5352adantl 452 . . . . . 6  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  N  e.  ( ZZ>= `  K )
)
54 eluzp1p1 10253 . . . . . 6  |-  ( N  e.  ( ZZ>= `  K
)  ->  ( N  +  1 )  e.  ( ZZ>= `  ( K  +  1 ) ) )
5553, 54syl 15 . . . . 5  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( N  +  1 )  e.  ( ZZ>= `  ( K  +  1 ) ) )
56 elfzuz 10794 . . . . . 6  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
5756adantl 452 . . . . 5  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  K  e.  ( ZZ>= `  M )
)
58 f1of 5472 . . . . . . . . . 10  |-  ( F : ( M ... ( N  +  1
) ) -1-1-onto-> ( M ... ( N  +  1 ) )  ->  F :
( M ... ( N  +  1 ) ) --> ( M ... ( N  +  1
) ) )
5917, 58syl 15 . . . . . . . . 9  |-  ( ph  ->  F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) ) )
60 fco 5398 . . . . . . . . 9  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> C  /\  F : ( M ... ( N  +  1 ) ) --> ( M ... ( N  +  1 ) ) )  ->  ( G  o.  F ) : ( M ... ( N  +  1
) ) --> C )
611, 59, 60syl2anc 642 . . . . . . . 8  |-  ( ph  ->  ( G  o.  F
) : ( M ... ( N  + 
1 ) ) --> C )
62 fss 5397 . . . . . . . 8  |-  ( ( ( G  o.  F
) : ( M ... ( N  + 
1 ) ) --> C  /\  C  C_  S
)  ->  ( G  o.  F ) : ( M ... ( N  +  1 ) ) --> S )
6361, 16, 62syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( G  o.  F
) : ( M ... ( N  + 
1 ) ) --> S )
64 ffvelrn 5663 . . . . . . 7  |-  ( ( ( G  o.  F
) : ( M ... ( N  + 
1 ) ) --> S  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  x )  e.  S
)
6563, 64sylan 457 . . . . . 6  |-  ( (
ph  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  x )  e.  S
)
6665adantlr 695 . . . . 5  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  (
( G  o.  F
) `  x )  e.  S )
6750, 51, 55, 57, 66seqsplit 11079 . . . 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 ) ) ) )
68 elfzp12 10861 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( K  e.  ( M ... N
)  <->  ( K  =  M  \/  K  e.  ( ( M  + 
1 ) ... N
) ) ) )
6968biimpa 470 . . . . . 6  |-  ( ( N  e.  ( ZZ>= `  M )  /\  K  e.  ( M ... N
) )  ->  ( K  =  M  \/  K  e.  ( ( M  +  1 ) ... N ) ) )
7015, 69sylan 457 . . . . 5  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( K  =  M  \/  K  e.  ( ( M  + 
1 ) ... N
) ) )
71 seqeq1 11049 . . . . . . . . . . 11  |-  ( K  =  M  ->  seq  K (  .+  ,  ( G  o.  F ) )  =  seq  M
(  .+  ,  ( G  o.  F )
) )
7271eqcomd 2288 . . . . . . . . . 10  |-  ( K  =  M  ->  seq  M (  .+  ,  ( G  o.  F ) )  =  seq  K
(  .+  ,  ( G  o.  F )
) )
7372fveq1d 5527 . . . . . . . . 9  |-  ( K  =  M  ->  (  seq  M (  .+  , 
( G  o.  F
) ) `  K
)  =  (  seq 
K (  .+  , 
( G  o.  F
) ) `  K
) )
74 f1ocnv 5485 . . . . . . . . . . . . 13  |-  ( F : ( M ... ( N  +  1
) ) -1-1-onto-> ( M ... ( N  +  1 ) )  ->  `' F : ( M ... ( N  +  1
) ) -1-1-onto-> ( M ... ( N  +  1 ) ) )
75 f1of 5472 . . . . . . . . . . . . 13  |-  ( `' F : ( M ... ( N  + 
1 ) ) -1-1-onto-> ( M ... ( N  + 
1 ) )  ->  `' F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) ) )
7617, 74, 753syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  `' F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) ) )
77 peano2uz 10272 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( N  +  1 )  e.  ( ZZ>= `  M )
)
78 eluzfz2 10804 . . . . . . . . . . . . 13  |-  ( ( N  +  1 )  e.  ( ZZ>= `  M
)  ->  ( N  +  1 )  e.  ( M ... ( N  +  1 ) ) )
7915, 77, 783syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  +  1 )  e.  ( M ... ( N  + 
1 ) ) )
80 ffvelrn 5663 . . . . . . . . . . . 12  |-  ( ( `' F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  ( N  + 
1 )  e.  ( M ... ( N  +  1 ) ) )  ->  ( `' F `  ( N  +  1 ) )  e.  ( M ... ( N  +  1
) ) )
8176, 79, 80syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F `  ( N  +  1
) )  e.  ( M ... ( N  +  1 ) ) )
8219, 81syl5eqel 2367 . . . . . . . . . 10  |-  ( ph  ->  K  e.  ( M ... ( N  + 
1 ) ) )
83 elfzelz 10798 . . . . . . . . . 10  |-  ( K  e.  ( M ... ( N  +  1
) )  ->  K  e.  ZZ )
84 seq1 11059 . . . . . . . . . 10  |-  ( K  e.  ZZ  ->  (  seq  K (  .+  , 
( G  o.  F
) ) `  K
)  =  ( ( G  o.  F ) `
 K ) )
8582, 83, 843syl 18 . . . . . . . . 9  |-  ( ph  ->  (  seq  K ( 
.+  ,  ( G  o.  F ) ) `
 K )  =  ( ( G  o.  F ) `  K
) )
8673, 85sylan9eqr 2337 . . . . . . . 8  |-  ( (
ph  /\  K  =  M )  ->  (  seq  M (  .+  , 
( G  o.  F
) ) `  K
)  =  ( ( G  o.  F ) `
 K ) )
8786oveq1d 5873 . . . . . . 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 ) ) ) )
88 simpr 447 . . . . . . . . 9  |-  ( (
ph  /\  K  =  M )  ->  K  =  M )
89 eluzfz1 10803 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... N ) )
9015, 89syl 15 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ( M ... N ) )
9190adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  K  =  M )  ->  M  e.  ( M ... N
) )
9288, 91eqeltrd 2357 . . . . . . . 8  |-  ( (
ph  /\  K  =  M )  ->  K  e.  ( M ... N
) )
9313adantlr 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  (
x  e.  C  /\  y  e.  C )
)  ->  ( x  .+  y )  =  ( y  .+  x ) )
9416adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  C  C_  S
)
9561adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( G  o.  F ) : ( M ... ( N  +  1 ) ) --> C )
9682adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  K  e.  ( M ... ( N  +  1 ) ) )
97 peano2uz 10272 . . . . . . . . . . 11  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K  +  1 )  e.  ( ZZ>= `  M )
)
98 fzss1 10830 . . . . . . . . . . 11  |-  ( ( K  +  1 )  e.  ( ZZ>= `  M
)  ->  ( ( K  +  1 ) ... ( N  + 
1 ) )  C_  ( M ... ( N  +  1 ) ) )
9957, 97, 983syl 18 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( ( K  +  1 ) ... ( N  + 
1 ) )  C_  ( M ... ( N  +  1 ) ) )
10050, 93, 51, 55, 94, 95, 96, 99seqf1olem2a 11084 . . . . . . . . 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 ) ) )
101 1z 10053 . . . . . . . . . . . 12  |-  1  e.  ZZ
102101a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  1  e.  ZZ )
103 elfzuz 10794 . . . . . . . . . . . . . . . . . 18  |-  ( K  e.  ( M ... ( N  +  1
) )  ->  K  e.  ( ZZ>= `  M )
)
104 fzss1 10830 . . . . . . . . . . . . . . . . . 18  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K ... N )  C_  ( M ... N ) )
10582, 103, 1043syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( K ... N
)  C_  ( M ... N ) )
106105sselda 3180 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  x  e.  ( M ... N ) )
107 ffvelrn 5663 . . . . . . . . . . . . . . . . 17  |-  ( ( J : ( M ... N ) --> ( M ... N )  /\  x  e.  ( M ... N ) )  ->  ( J `  x )  e.  ( M ... N ) )
10822, 107sylan 457 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( J `  x )  e.  ( M ... N ) )
109106, 108syldan 456 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( J `  x )  e.  ( M ... N ) )
110 fvres 5542 . . . . . . . . . . . . . . 15  |-  ( ( J `  x )  e.  ( M ... N )  ->  (
( G  |`  ( M ... N ) ) `
 ( J `  x ) )  =  ( G `  ( J `  x )
) )
111109, 110syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( ( G  |`  ( M ... N ) ) `  ( J `  x ) )  =  ( G `
 ( J `  x ) ) )
112 breq1 4026 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  x  ->  (
k  <  K  <->  x  <  K ) )
113 id 19 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  x  ->  k  =  x )
114 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  x  ->  (
k  +  1 )  =  ( x  + 
1 ) )
115112, 113, 114ifbieq12d 3587 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  x  ->  if ( k  <  K ,  k ,  ( k  +  1 ) )  =  if ( x  <  K ,  x ,  ( x  +  1 ) ) )
116115fveq2d 5529 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  x  ->  ( F `  if (
k  <  K , 
k ,  ( k  +  1 ) ) )  =  ( F `
 if ( x  <  K ,  x ,  ( x  + 
1 ) ) ) )
117 fvex 5539 . . . . . . . . . . . . . . . . . 18  |-  ( F `
 if ( x  <  K ,  x ,  ( x  + 
1 ) ) )  e.  _V
118116, 18, 117fvmpt 5602 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( M ... N )  ->  ( J `  x )  =  ( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) ) )
119106, 118syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( J `  x )  =  ( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) ) )
120 elfzle1 10799 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( K ... N )  ->  K  <_  x )
121120adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  K  <_  x )
12282, 83syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  K  e.  ZZ )
123122zred 10117 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K  e.  RR )
124123adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  K  e.  RR )
125 elfzelz 10798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( K ... N )  ->  x  e.  ZZ )
126125adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  x  e.  ZZ )
127126zred 10117 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  x  e.  RR )
128124, 127lenltd 8965 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( K  <_  x  <->  -.  x  <  K ) )
129121, 128mpbid 201 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  -.  x  <  K )
130 iffalse 3572 . . . . . . . . . . . . . . . . . 18  |-  ( -.  x  <  K  ->  if ( x  <  K ,  x ,  ( x  +  1 ) )  =  ( x  + 
1 ) )
131130fveq2d 5529 . . . . . . . . . . . . . . . . 17  |-  ( -.  x  <  K  -> 
( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) )  =  ( F `
 ( x  + 
1 ) ) )
132129, 131syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( F `  if ( x  < 
K ,  x ,  ( x  +  1 ) ) )  =  ( F `  (
x  +  1 ) ) )
133119, 132eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( J `  x )  =  ( F `  ( x  +  1 ) ) )
134133fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( G `  ( J `  x
) )  =  ( G `  ( F `
 ( x  + 
1 ) ) ) )
135111, 134eqtrd 2315 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( ( G  |`  ( M ... N ) ) `  ( J `  x ) )  =  ( G `
 ( F `  ( x  +  1
) ) ) )
136 fvco3 5596 . . . . . . . . . . . . . . 15  |-  ( ( J : ( M ... N ) --> ( M ... N )  /\  x  e.  ( M ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
13722, 136sylan 457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
138106, 137syldan 456 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
139 fzp1elp1 10839 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( M ... N )  ->  (
x  +  1 )  e.  ( M ... ( N  +  1
) ) )
140106, 139syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( x  +  1 )  e.  ( M ... ( N  +  1 ) ) )
141 fvco3 5596 . . . . . . . . . . . . . . 15  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  ( x  + 
1 )  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  ( x  +  1 ) )  =  ( G `  ( F `
 ( x  + 
1 ) ) ) )
14259, 141sylan 457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  +  1 )  e.  ( M ... ( N  +  1 ) ) )  ->  (
( G  o.  F
) `  ( x  +  1 ) )  =  ( G `  ( F `  ( x  +  1 ) ) ) )
143140, 142syldan 456 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( ( G  o.  F ) `  ( x  +  1 ) )  =  ( G `  ( F `
 ( x  + 
1 ) ) ) )
144135, 138, 1433eqtr4d 2325 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  o.  F
) `  ( x  +  1 ) ) )
145144adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  x  e.  ( K ... N
) )  ->  (
( ( G  |`  ( M ... N ) )  o.  J ) `
 x )  =  ( ( G  o.  F ) `  (
x  +  1 ) ) )
14653, 102, 145seqshft2 11072 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  (  seq  K (  .+  ,  ( ( G  |`  ( M ... N ) )  o.  J ) ) `
 N )  =  (  seq  ( K  +  1 ) ( 
.+  ,  ( G  o.  F ) ) `
 ( N  + 
1 ) ) )
147 fvco3 5596 . . . . . . . . . . . . 13  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  K  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  K )  =  ( G `  ( F `
 K ) ) )
14859, 82, 147syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( G  o.  F ) `  K
)  =  ( G `
 ( F `  K ) ) )
14919fveq2i 5528 . . . . . . . . . . . . . 14  |-  ( F `
 K )  =  ( F `  ( `' F `  ( N  +  1 ) ) )
150 f1ocnvfv2 5793 . . . . . . . . . . . . . . 15  |-  ( ( F : ( M ... ( N  + 
1 ) ) -1-1-onto-> ( M ... ( N  + 
1 ) )  /\  ( N  +  1
)  e.  ( M ... ( N  + 
1 ) ) )  ->  ( F `  ( `' F `  ( N  +  1 ) ) )  =  ( N  +  1 ) )
15117, 79, 150syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  ( `' F `  ( N  +  1 ) ) )  =  ( N  +  1 ) )
152149, 151syl5eq 2327 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F `  K
)  =  ( N  +  1 ) )
153152fveq2d 5529 . . . . . . . . . . . 12  |-  ( ph  ->  ( G `  ( F `  K )
)  =  ( G `
 ( N  + 
1 ) ) )
154148, 153eqtr2d 2316 . . . . . . . . . . 11  |-  ( ph  ->  ( G `  ( N  +  1 ) )  =  ( ( G  o.  F ) `
 K ) )
155154adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( G `  ( N  +  1 ) )  =  ( ( G  o.  F
) `  K )
)
156146, 155oveq12d 5876 . . . . . . . . 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 ) ) )
157100, 156eqtr4d 2318 . . . . . . . 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
) ) ) )
15892, 157syldan 456 . . . . . . 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 ) ) ) )
15988seqeq1d 11052 . . . . . . . . 9  |-  ( (
ph  /\  K  =  M )  ->  seq  K (  .+  ,  ( ( G  |`  ( M ... N ) )  o.  J ) )  =  seq  M ( 
.+  ,  ( ( G  |`  ( M ... N ) )  o.  J ) ) )
160159fveq1d 5527 . . . . . . . 8  |-  ( (
ph  /\  K  =  M )  ->  (  seq  K (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  =  (  seq  M
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) `
 N ) )
161160oveq1d 5873 . . . . . . 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 ) ) ) )
16287, 158, 1613eqtrd 2319 . . . . . 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 ) ) ) )
163 eluzel2 10235 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
16415, 163syl 15 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ZZ )
165 elfzuz 10794 . . . . . . . . . . 11  |-  ( K  e.  ( ( M  +  1 ) ... N )  ->  K  e.  ( ZZ>= `  ( M  +  1 ) ) )
166 eluzp1m1 10251 . . . . . . . . . . 11  |-  ( ( M  e.  ZZ  /\  K  e.  ( ZZ>= `  ( M  +  1
) ) )  -> 
( K  -  1 )  e.  ( ZZ>= `  M ) )
167164, 165, 166syl2an 463 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  ( K  -  1 )  e.  ( ZZ>= `  M
) )
168 eluzelz 10238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
16915, 168syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  ZZ )
170169zcnd 10118 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  CC )
171 ax-1cn 8795 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
172 pncan 9057 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
173170, 171, 172sylancl 643 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  N )
174 peano2zm 10062 . . . . . . . . . . . . . . . . . . . 20  |-  ( K  e.  ZZ  ->  ( K  -  1 )  e.  ZZ )
17582, 83, 1743syl 18 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( K  -  1 )  e.  ZZ )
176 elfzuz3 10795 . . . . . . . . . . . . . . . . . . . . 21  |-  ( K  e.  ( M ... ( N  +  1
) )  ->  ( N  +  1 )  e.  ( ZZ>= `  K
) )
17782, 176syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= `  K ) )
178122zcnd 10118 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  K  e.  CC )
179 npcan 9060 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( K  e.  CC  /\  1  e.  CC )  ->  ( ( K  - 
1 )  +  1 )  =  K )
180178, 171, 179sylancl 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( K  - 
1 )  +  1 )  =  K )
181180fveq2d 5529 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ZZ>= `  ( ( K  -  1 )  +  1 ) )  =  ( ZZ>= `  K
) )
182177, 181eleqtrrd 2360 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= `  ( ( K  - 
1 )  +  1 ) ) )
183 eluzp1m1 10251 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( K  -  1 )  e.  ZZ  /\  ( N  +  1
)  e.  ( ZZ>= `  ( ( K  - 
1 )  +  1 ) ) )  -> 
( ( N  + 
1 )  -  1 )  e.  ( ZZ>= `  ( K  -  1
) ) )
184175, 182, 183syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  e.  ( ZZ>= `  ( K  -  1
) ) )
185173, 184eqeltrrd 2358 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  ( ZZ>= `  ( K  -  1
) ) )
186 fzss2 10831 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  ( K  -  1 ) )  ->  ( M ... ( K  -  1 ) )  C_  ( M ... N ) )
187185, 186syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( M ... ( K  -  1 ) )  C_  ( M ... N ) )
188187sselda 3180 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  x  e.  ( M ... N ) )
189188, 108syldan 456 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  x )  e.  ( M ... N ) )
190189, 110syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( ( G  |`  ( M ... N ) ) `  ( J `  x ) )  =  ( G `
 ( J `  x ) ) )
191188, 118syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  x )  =  ( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) ) )
192 elfzm11 10853 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  e.  ZZ  /\  K  e.  ZZ )  ->  ( x  e.  ( M ... ( K  -  1 ) )  <-> 
( x  e.  ZZ  /\  M  <_  x  /\  x  <  K ) ) )
193164, 122, 192syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( x  e.  ( M ... ( K  -  1 ) )  <-> 
( x  e.  ZZ  /\  M  <_  x  /\  x  <  K ) ) )
194193biimpa 470 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( x  e.  ZZ  /\  M  <_  x  /\  x  <  K
) )
195194simp3d 969 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  x  <  K )
196 iftrue 3571 . . . . . . . . . . . . . . . . 17  |-  ( x  <  K  ->  if ( x  <  K ,  x ,  ( x  +  1 ) )  =  x )
197196fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( x  <  K  ->  ( F `  if (
x  <  K ,  x ,  ( x  +  1 ) ) )  =  ( F `
 x ) )
198195, 197syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( F `  if ( x  < 
K ,  x ,  ( x  +  1 ) ) )  =  ( F `  x
) )
199191, 198eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  x )  =  ( F `  x ) )
200199fveq2d 5529 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( J `  x
) )  =  ( G `  ( F `
 x ) ) )
201190, 200eqtr2d 2316 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( F `  x
) )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
202 peano2uz 10272 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  ( K  -  1 ) )  ->  ( N  +  1 )  e.  ( ZZ>= `  ( K  -  1 ) ) )
203 fzss2 10831 . . . . . . . . . . . . . . 15  |-  ( ( N  +  1 )  e.  ( ZZ>= `  ( K  -  1 ) )  ->  ( M ... ( K  -  1 ) )  C_  ( M ... ( N  + 
1 ) ) )
204185, 202, 2033syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M ... ( K  -  1 ) )  C_  ( M ... ( N  +  1 ) ) )
205204sselda 3180 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  x  e.  ( M ... ( N  +  1 ) ) )
206 fvco3 5596 . . . . . . . . . . . . . 14  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  x )  =  ( G `  ( F `
 x ) ) )
20759, 206sylan 457 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  x )  =  ( G `  ( F `
 x ) ) )
208205, 207syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( ( G  o.  F ) `  x )  =  ( G `  ( F `
 x ) ) )
209188, 137syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
210201, 208, 2093eqtr4d 2325 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( ( G  o.  F ) `  x )  =  ( ( ( G  |`  ( M ... N ) )  o.  J ) `
 x ) )
211210adantlr 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  (
( G  o.  F
) `  x )  =  ( ( ( G  |`  ( M ... N ) )  o.  J ) `  x
) )
212167, 211seqfveq 11070 . . . . . . . . 9  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq  M (  .+  , 
( G  o.  F
) ) `  ( K  -  1 ) )  =  (  seq 
M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  ( K  -  1 ) ) )
213 fzp1ss 10837 . . . . . . . . . . . 12  |-  ( M  e.  ZZ  ->  (
( M  +  1 ) ... N ) 
C_  ( M ... N ) )
21415, 163, 2133syl 18 . . . . . . . . . . 11  |-  ( ph  ->  ( ( M  + 
1 ) ... N
)  C_  ( M ... N ) )
215214sselda 3180 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  K  e.  ( M ... N
) )
216215, 157syldan 456 . . . . . . . . 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 ) ) ) )
217212, 216oveq12d 5876 . . . . . . . 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 ) ) ) ) )
218205, 65syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( ( G  o.  F ) `  x )  e.  S
)
219218adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  (
( G  o.  F
) `  x )  e.  S )
22012adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  .+  y )  e.  S
)
221167, 219, 220seqcl 11066 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq  M (  .+  , 
( G  o.  F
) ) `  ( K  -  1 ) )  e.  S )
222 ffvelrn 5663 . . . . . . . . . . . . 13  |-  ( ( ( G  o.  F
) : ( M ... ( N  + 
1 ) ) --> C  /\  K  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  K )  e.  C
)
22361, 82, 222syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( G  o.  F ) `  K
)  e.  C )
22416, 223sseldd 3181 . . . . . . . . . . 11  |-  ( ph  ->  ( ( G  o.  F ) `  K
)  e.  S )
225224adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (
( G  o.  F
) `  K )  e.  S )
22699sselda 3180 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  x  e.  ( ( K  + 
1 ) ... ( N  +  1 ) ) )  ->  x  e.  ( M ... ( N  +  1 ) ) )
227226, 66syldan 456 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  x  e.  ( ( K  + 
1 ) ... ( N  +  1 ) ) )  ->  (
( G  o.  F
) `  x )  e.  S )
22855, 227, 50seqcl 11066 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  (  seq  ( K  +  1
) (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  e.  S )
229215, 228syldan 456 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq  ( K  +  1 ) (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  e.  S )
230221, 225, 2293jca 1132 . . . . . . . . 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
) )
23114caovassg 6018 . . . . . . . . 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
) ) ) ) )
232230, 231syldan 456 . . . . . . . 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
) ) ) ) )
233 fss 5397 . . . . . . . . . . . . . . . . 17  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> C  /\  C  C_  S
)  ->  G :
( M ... ( N  +  1 ) ) --> S )
2341, 16, 233syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G : ( M ... ( N  + 
1 ) ) --> S )
235 fssres 5408 . . . . . . . . . . . . . . . 16  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> S  /\  ( M ... N )  C_  ( M ... ( N  + 
1 ) ) )  ->  ( G  |`  ( M ... N ) ) : ( M ... N ) --> S )
236234, 4, 235sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G  |`  ( M ... N ) ) : ( M ... N ) --> S )
237 fco 5398 . . . . . . . . . . . . . . 15  |-  ( ( ( G  |`  ( M ... N ) ) : ( M ... N ) --> S  /\  J : ( M ... N ) --> ( M ... N ) )  ->  ( ( G  |`  ( M ... N
) )  o.  J
) : ( M ... N ) --> S )
238236, 22, 237syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G  |`  ( M ... N ) )  o.  J ) : ( M ... N ) --> S )
239 ffvelrn 5663 . . . . . . . . . . . . . 14  |-  ( ( ( ( G  |`  ( M ... N ) )  o.  J ) : ( M ... N ) --> S  /\  x  e.  ( M ... N ) )  -> 
( ( ( G  |`  ( M ... N
) )  o.  J
) `  x )  e.  S )
240238, 239sylan 457 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  e.  S
)
241188, 240syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  e.  S
)
242241adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  (
( ( G  |`  ( M ... N ) )  o.  J ) `
 x )  e.  S )
243167, 242, 220seqcl 11066 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq  M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  ( K  -  1 ) )  e.  S )
244 elfzuz3 10795 . . . . . . . . . . . 12  |-  ( K  e.  ( ( M  +  1 ) ... N )  ->  N  e.  ( ZZ>= `  K )
)
245244adantl 452 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  N  e.  ( ZZ>= `  K )
)
246106, 240syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  e.  S
)
247246adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( K ... N
) )  ->  (
( ( G  |`  ( M ... N ) )  o.  J ) `
 x )  e.  S )
248245, 247, 220seqcl 11066 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq  K (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  e.  S )
249 ffvelrn 5663 . . . . . . . . . . . 12  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> S  /\  ( N  + 
1 )  e.  ( M ... ( N  +  1 ) ) )  ->  ( G `  ( N  +  1 ) )  e.  S
)
250234, 79, 249syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( G `  ( N  +  1 ) )  e.  S )
251250adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  ( G `  ( N  +  1 ) )  e.  S )
252243, 248, 2513jca 1132 . . . . . . . . 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 ) )
25314caovassg 6018 . . . . . . . . 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
) ) ) ) )
254252, 253syldan 456 . . . . . . . 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 ) ) ) ) )
255217, 232, 2543eqtr4d 2325 . . . . . . 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
) ) ) )
256 seqm1 11063 . . . . . . . . 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
) ) )
257164, 165, 256syl2an 463 . . . . . . . 8  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq  M (  .+  , 
( G  o.  F
) ) `  K
)  =  ( (  seq  M (  .+  ,  ( G  o.  F ) ) `  ( K  -  1
) )  .+  (
( G  o.  F
) `  K )
) )
258257oveq1d 5873 . . . . . . 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
) ) ) )
25914adantlr 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  (
x  e.  S  /\  y  e.  S  /\  z  e.  S )
)  ->  ( (
x  .+  y )  .+  z )  =  ( x  .+  ( y 
.+  z ) ) )
260 elfzelz 10798 . . . . . . . . . . . . . . 15  |-  ( K  e.  ( ( M  +  1 ) ... N )  ->  K  e.  ZZ )
261260adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  K  e.  ZZ )
262261zcnd 10118 . . . . . . . . . . . . 13  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  K  e.  CC )
263262, 171, 179sylancl 643 . . . . . . . . . . . 12  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (
( K  -  1 )  +  1 )  =  K )
264263fveq2d 5529 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  ( ZZ>=
`  ( ( K  -  1 )  +  1 ) )  =  ( ZZ>= `  K )
)
265245, 264eleqtrrd 2360 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  N  e.  ( ZZ>= `  ( ( K  -  1 )  +  1 ) ) )
266240adantlr 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( M ... N
) )  ->  (
( ( G  |`  ( M ... N ) )  o.  J ) `
 x )  e.  S )
267220, 259, 265, 167, 266seqsplit 11079 . . . . . . . . 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 ) ) )
268263seqeq1d 11052 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  seq  ( ( K  - 
1 )  +  1 ) (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) )  =  seq  K
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) )
269268fveq1d 5527 . . . . . . . . . 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 ) )
270269oveq2d 5874 . . . . . . . . 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 ) ) )
271267, 270eqtrd 2315 . . . . . . . 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 ) ) )
272271oveq1d 5873 . . . . . . 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
) ) ) )
273255, 258, 2723eqtr4d 2325 . . . . . 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 ) ) ) )
274162, 273jaodan 760 . . . . 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
) ) ) )
27570, 274syldan 456 . . . 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 ) ) ) )
27667, 275eqtrd 2315 . . 3  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  (  seq  M (  .+  ,  ( G  o.  F ) ) `  ( N  +  1 ) )  =  ( (  seq 
M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N ) 
.+  ( G `  ( N  +  1
) ) ) )
27715adantr 451 . . . . 5  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  N  e.  ( ZZ>= `  M )
)
278 seqp1 11061 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  (  seq  M (  .+  ,  ( G  o.  F ) ) `  ( N  +  1 ) )  =  ( (  seq 
M (  .+  , 
( G  o.  F
) ) `  N
)  .+  ( ( G  o.  F ) `  ( N  +  1 ) ) ) )
279277, 278syl 15 . . . 4  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (  seq  M (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  =  ( (  seq  M (  .+  ,  ( G  o.  F ) ) `  N )  .+  (
( G  o.  F
) `  ( N  +  1 ) ) ) )
280118adantl 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( J `  x
)  =  ( F `
 if ( x  <  K ,  x ,  ( x  + 
1 ) ) ) )
281 elfzelz 10798 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( M ... N )  ->  x  e.  ZZ )
282281zred 10117 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( M ... N )  ->  x  e.  RR )
283282adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  x  e.  RR )
284169zred 10117 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  RR )
285284adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  N  e.  RR )
286 peano2re 8985 . . . . . . . . . . . . . . 15  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
287285, 286syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( N  +  1 )  e.  RR )
288 elfzle2 10800 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( M ... N )  ->  x  <_  N )
289288adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  x  <_  N )
290285ltp1d 9687 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  N  <  ( N  +  1 ) )
291283, 285, 287, 289, 290lelttrd 8974 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  x  <  ( N  +  1 ) )
292291adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  x  <  ( N  + 
1 ) )
293 simplr 731 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  K  =  ( N  +  1 ) )
294292, 293breqtrrd 4049 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  x  <  K )
295294, 197syl 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) )  =  ( F `
 x ) )
296280, 295eqtrd 2315 . . . . . . . . 9  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( J `  x
)  =  ( F `
 x ) )
297296fveq2d 5529 . . . . . . . 8  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( G  |`  ( M ... N ) ) `  ( J `
 x ) )  =  ( ( G  |`  ( M ... N
) ) `  ( F `  x )
) )
298282adantl 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  x  e.  RR )
299298, 294gtned 8954 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  K  =/=  x )
30059ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  F : ( M ... ( N  +  1
) ) --> ( M ... ( N  + 
1 ) ) )
301 fzelp1 10838 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( M ... N )  ->  x  e.  ( M ... ( N  +  1 ) ) )
302301adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  x  e.  ( M ... ( N  +  1 ) ) )
303 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  ( F `  x )  e.  ( M ... ( N  +  1 ) ) )
304300, 302, 303syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( F `  x
)  e.  ( M ... ( N  + 
1 ) ) )
30515ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  N  e.  ( ZZ>= `  M ) )
306 elfzp1 10836 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ( F `  x )  e.  ( M ... ( N  +  1 ) )  <->  ( ( F `
 x )  e.  ( M ... N
)  \/  ( F `
 x )  =  ( N  +  1 ) ) ) )
307305, 306syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( F `  x )  e.  ( M ... ( N  +  1 ) )  <-> 
( ( F `  x )  e.  ( M ... N )  \/  ( F `  x )  =  ( N  +  1 ) ) ) )
308304, 307mpbid 201 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( F `  x )  e.  ( M ... N )  \/  ( F `  x )  =  ( N  +  1 ) ) )
309308ord 366 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( -.  ( F `
 x )  e.  ( M ... N
)  ->  ( F `  x )  =  ( N  +  1 ) ) )
31017ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  F : ( M ... ( N  +  1
) ) -1-1-onto-> ( M ... ( N  +  1 ) ) )
311 f1ocnvfv 5794 . . . . . . . . . . . . . 14  |-  ( ( F : ( M ... ( N  + 
1 ) ) -1-1-onto-> ( M ... ( N  + 
1 ) )  /\  x  e.  ( M ... ( N  +  1 ) ) )  -> 
( ( F `  x )  =  ( N  +  1 )  ->  ( `' F `  ( N  +  1 ) )  =  x ) )
312310, 302, 311syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( F `  x )  =  ( N  +  1 )  ->  ( `' F `  ( N  +  1 ) )  =  x ) )
31319eqeq1i 2290 . . . . . . . . . . . . 13  |-  ( K  =  x  <->  ( `' F `  ( N  +  1 ) )  =  x )
314312, 313syl6ibr 218 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( F `  x )  =  ( N  +  1 )  ->  K  =  x ) )
315309, 314syld 40 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( -.  ( F `
 x )  e.  ( M ... N
)  ->  K  =  x ) )
316315necon1ad 2513 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( K  =/=  x  ->  ( F `  x
)  e.  ( M ... N ) ) )
317299, 316mpd 14 . . . . . . . . 9  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( F `  x
)  e.  ( M ... N ) )
318 fvres 5542 . . . . . . . . 9  |-  ( ( F `  x )  e.  ( M ... N )  ->  (
( G  |`  ( M ... N ) ) `
 ( F `  x ) )  =  ( G `  ( F `  x )
) )
319317, 318syl 15 . . . . . . . 8  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( G  |`  ( M ... N ) ) `  ( F `
 x ) )  =  ( G `  ( F `  x ) ) )
320297, 319eqtr2d 2316 . . . . . . 7  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( G `  ( F `  x )
)  =  ( ( G  |`  ( M ... N ) ) `  ( J `  x ) ) )
32159, 301, 206syl2an 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( ( G  o.  F ) `  x )  =  ( G `  ( F `
 x ) ) )
322321adantlr 695 . . . . . . 7  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( G  o.  F ) `  x
)  =  ( G `
 ( F `  x ) ) )
323137adantlr 695 . . . . . . 7  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( ( G  |`  ( M ... N
) )  o.  J
) `  x )  =  ( ( G  |`  ( M ... N
) ) `  ( J `  x )
) )
324320, 322, 3233eqtr4d 2325 . . . . . 6  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( G  o.  F ) `  x
)  =  ( ( ( G  |`  ( M ... N ) )  o.  J ) `  x ) )
325277, 324seqfveq 11070 . . . . 5  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (  seq  M (  .+  , 
( G  o.  F
) ) `  N
)  =  (  seq 
M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N ) )
326 fvco3 5596 . . . . . . . 8  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  ( N  + 
1 )  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  ( N  +  1 ) )  =  ( G `  ( F `
 ( N  + 
1 ) ) ) )
32759, 79, 326syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( ( G  o.  F ) `  ( N  +  1 ) )  =  ( G `
 ( F `  ( N  +  1
) ) ) )
328327adantr 451 . . . . . 6  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (
( G  o.  F
) `  ( N  +  1 ) )  =  ( G `  ( F `  ( N  +  1 ) ) ) )
329 simpr 447 . . . . . . . . . 10  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  K  =  ( N  + 
1 ) )
33019, 329syl5eqr 2329 . . . . . . . . 9  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( `' F `  ( N  +  1 ) )  =  ( N  + 
1 ) )
331330fveq2d 5529 . . . . . . . 8  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( F `  ( `' F `  ( N  +  1 ) ) )  =  ( F `
 ( N  + 
1 ) ) )
332151adantr 451 . . . . . . . 8  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( F `  ( `' F `  ( N  +  1 ) ) )  =  ( N  +  1 ) )
333331, 332eqtr3d 2317 . . . . . . 7  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( F `  ( N  +  1 ) )  =  ( N  + 
1 ) )
334333fveq2d 5529 . . . . . 6  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( G `  ( F `  ( N  +  1 ) ) )  =  ( G `  ( N  +  1 ) ) )
335328, 334eqtrd 2315 . . . . 5  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (
( G  o.  F
) `  ( N  +  1 ) )  =  ( G `  ( N  +  1
) ) )
336325, 335oveq12d 5876 . . . 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 ) ) ) )
337279, 336eqtrd 2315 . . 3  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (  seq  M (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  =  ( (  seq  M (  .+  ,  ( ( G  |`  ( M ... N
) )  o.  J
) ) `  N
)  .+  ( G `  ( N  +  1 ) ) ) )
338 elfzp1 10836 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( K  e.  ( M ... ( N  +  1 ) )  <->  ( K  e.  ( M ... N
)  \/  K  =  ( N  +  1 ) ) ) )
33915, 338syl 15 . . . 4  |-  ( ph  ->  ( K  e.  ( M ... ( N  +  1 ) )  <-> 
( K  e.  ( M ... N )  \/  K  =  ( N  +  1 ) ) ) )
34082, 339mpbid 201 . . 3  |-  ( ph  ->  ( K  e.  ( M ... N )  \/  K  =  ( N  +  1 ) ) )
341276, 337, 340mpjaodan 761 . 2  |-  ( ph  ->  (  seq  M ( 
.+  ,  ( G  o.  F ) ) `
 ( N  + 
1 ) )  =  ( (  seq  M
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) `
 N )  .+  ( G `  ( N  +  1 ) ) ) )
342 seqp1 11061 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  (  seq  M (  .+  ,  G
) `  ( N  +  1 ) )  =  ( (  seq 
M (  .+  ,  G ) `  N
)  .+  ( G `  ( N  +  1 ) ) ) )
34315, 342syl 15 . 2  |-  ( ph  ->  (  seq  M ( 
.+  ,  G ) `
 ( N  + 
1 ) )  =  ( (  seq  M
(  .+  ,  G
) `  N )  .+  ( G `  ( N  +  1 ) ) ) )
34449, 341, 3433eqtr4d 2325 1  |-  ( ph  ->  (  seq  M ( 
.+  ,  ( G  o.  F ) ) `
 ( N  + 
1 ) )  =  (  seq  M ( 
.+  ,  G ) `
 ( N  + 
1 ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934   A.wal 1527    = wceq 1623    e. wcel 1684    =/= wne 2446   _Vcvv 2788    C_ wss 3152   ifcif 3565   class class class wbr 4023    e. cmpt 4077   `'ccnv 4688    |` cres 4691    o. ccom 4693    Fn wfn 5250   -->wf 5251   -1-1-onto->wf1o 5254   ` cfv 5255  (class class class)co 5858   Fincfn 6863   CCcc 8735   RRcr 8736   1c1 8738    + caddc 8740    < clt 8867    <_ cle 8868    - cmin 9037   ZZcz 10024   ZZ>=cuz 10230   ...cfz 10782    seq cseq 11046
This theorem is referenced by:  seqf1o  11087
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-n0 9966  df-z 10025  df-uz 10231  df-fz 10783  df-fzo 10871  df-seq 11047
  Copyright terms: Public domain W3C validator