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

Theorem seqf1olem2 12115
Description: Lemma for seqf1o 12116. (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 5731 . . . . . . . . . 10  |-  ( G : ( M ... ( N  +  1
) ) --> C  ->  G  Fn  ( M ... ( N  +  1 ) ) )
31, 2syl 16 . . . . . . . . 9  |-  ( ph  ->  G  Fn  ( M ... ( N  + 
1 ) ) )
4 fzssp1 11726 . . . . . . . . 9  |-  ( M ... N )  C_  ( M ... ( N  +  1 ) )
5 fnssres 5694 . . . . . . . . 9  |-  ( ( G  Fn  ( M ... ( N  + 
1 ) )  /\  ( M ... N ) 
C_  ( M ... ( N  +  1
) ) )  -> 
( G  |`  ( M ... N ) )  Fn  ( M ... N ) )
63, 4, 5sylancl 662 . . . . . . . 8  |-  ( ph  ->  ( G  |`  ( M ... N ) )  Fn  ( M ... N ) )
7 fzfid 12051 . . . . . . . 8  |-  ( ph  ->  ( M ... N
)  e.  Fin )
8 fnfi 7798 . . . . . . . 8  |-  ( ( ( G  |`  ( M ... N ) )  Fn  ( M ... N )  /\  ( M ... N )  e. 
Fin )  ->  ( G  |`  ( M ... N ) )  e. 
Fin )
96, 7, 8syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( G  |`  ( M ... N ) )  e.  Fin )
10 elex 3122 . . . . . . 7  |-  ( ( G  |`  ( M ... N ) )  e. 
Fin  ->  ( G  |`  ( M ... N ) )  e.  _V )
119, 10syl 16 . . . . . 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 12114 . . . . . . . 8  |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )
21 f1of 5816 . . . . . . . 8  |-  ( J : ( M ... N ) -1-1-onto-> ( M ... N
)  ->  J :
( M ... N
) --> ( M ... N ) )
2220, 21syl 16 . . . . . . 7  |-  ( ph  ->  J : ( M ... N ) --> ( M ... N ) )
23 fex2 6739 . . . . . . 7  |-  ( ( J : ( M ... N ) --> ( M ... N )  /\  ( M ... N )  e.  Fin  /\  ( M ... N
)  e.  Fin )  ->  J  e.  _V )
2422, 7, 7, 23syl3anc 1228 . . . . . 6  |-  ( ph  ->  J  e.  _V )
2511, 24jca 532 . . . . 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 5751 . . . . . . 7  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> C  /\  ( M ... N )  C_  ( M ... ( N  + 
1 ) ) )  ->  ( G  |`  ( M ... N ) ) : ( M ... N ) --> C )
281, 4, 27sylancl 662 . . . . . 6  |-  ( ph  ->  ( G  |`  ( M ... N ) ) : ( M ... N ) --> C )
2920, 28jca 532 . . . . 5  |-  ( ph  ->  ( J : ( M ... N ) -1-1-onto-> ( M ... N )  /\  ( G  |`  ( M ... N ) ) : ( M ... N ) --> C ) )
30 f1oeq1 5807 . . . . . . . 8  |-  ( f  =  J  ->  (
f : ( M ... N ) -1-1-onto-> ( M ... N )  <->  J :
( M ... N
)
-1-1-onto-> ( M ... N ) ) )
31 feq1 5713 . . . . . . . 8  |-  ( g  =  ( G  |`  ( M ... N ) )  ->  ( g : ( M ... N ) --> C  <->  ( G  |`  ( M ... N
) ) : ( M ... N ) --> C ) )
3230, 31bi2anan9r 872 . . . . . . 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 5160 . . . . . . . . . . 11  |-  ( g  =  ( G  |`  ( M ... N ) )  ->  ( g  o.  f )  =  ( ( G  |`  ( M ... N ) )  o.  f ) )
34 coeq2 5161 . . . . . . . . . . 11  |-  ( f  =  J  ->  (
( G  |`  ( M ... N ) )  o.  f )  =  ( ( G  |`  ( M ... N ) )  o.  J ) )
3533, 34sylan9eq 2528 . . . . . . . . . 10  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  (
g  o.  f )  =  ( ( G  |`  ( M ... N
) )  o.  J
) )
3635seqeq3d 12083 . . . . . . . . 9  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  seq M (  .+  , 
( g  o.  f
) )  =  seq M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) )
3736fveq1d 5868 . . . . . . . 8  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  N
)  =  (  seq M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N ) )
38 simpl 457 . . . . . . . . . 10  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  g  =  ( G  |`  ( M ... N ) ) )
3938seqeq3d 12083 . . . . . . . . 9  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  seq M (  .+  , 
g )  =  seq M (  .+  , 
( G  |`  ( M ... N ) ) ) )
4039fveq1d 5868 . . . . . . . 8  |-  ( ( g  =  ( G  |`  ( M ... N
) )  /\  f  =  J )  ->  (  seq M (  .+  , 
g ) `  N
)  =  (  seq M (  .+  , 
( G  |`  ( M ... N ) ) ) `  N ) )
4137, 40eqeq12d 2489 . . . . . . 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 320 . . . . . 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 3201 . . . . 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 61 . . . 4  |-  ( ph  ->  (  seq M ( 
.+  ,  ( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  =  (  seq M (  .+  ,  ( G  |`  ( M ... N ) ) ) `  N
) )
45 fvres 5880 . . . . . 6  |-  ( x  e.  ( M ... N )  ->  (
( G  |`  ( M ... N ) ) `
 x )  =  ( G `  x
) )
4645adantl 466 . . . . 5  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( ( G  |`  ( M ... N ) ) `  x )  =  ( G `  x ) )
4715, 46seqfveq 12099 . . . 4  |-  ( ph  ->  (  seq M ( 
.+  ,  ( G  |`  ( M ... N
) ) ) `  N )  =  (  seq M (  .+  ,  G ) `  N
) )
4844, 47eqtrd 2508 . . 3  |-  ( ph  ->  (  seq M ( 
.+  ,  ( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  =  (  seq M (  .+  ,  G ) `  N
) )
4948oveq1d 6299 . 2  |-  ( ph  ->  ( (  seq M
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) `
 N )  .+  ( G `  ( N  +  1 ) ) )  =  ( (  seq M (  .+  ,  G ) `  N
)  .+  ( G `  ( N  +  1 ) ) ) )
5012adantlr 714 . . . . 5  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  .+  y )  e.  S
)
5114adantlr 714 . . . . 5  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  (
x  e.  S  /\  y  e.  S  /\  z  e.  S )
)  ->  ( (
x  .+  y )  .+  z )  =  ( x  .+  ( y 
.+  z ) ) )
52 elfzuz3 11685 . . . . . . 7  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
5352adantl 466 . . . . . 6  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  N  e.  ( ZZ>= `  K )
)
54 eluzp1p1 11107 . . . . . 6  |-  ( N  e.  ( ZZ>= `  K
)  ->  ( N  +  1 )  e.  ( ZZ>= `  ( K  +  1 ) ) )
5553, 54syl 16 . . . . 5  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( N  +  1 )  e.  ( ZZ>= `  ( K  +  1 ) ) )
56 elfzuz 11684 . . . . . 6  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
5756adantl 466 . . . . 5  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  K  e.  ( ZZ>= `  M )
)
58 f1of 5816 . . . . . . . . . 10  |-  ( F : ( M ... ( N  +  1
) ) -1-1-onto-> ( M ... ( N  +  1 ) )  ->  F :
( M ... ( N  +  1 ) ) --> ( M ... ( N  +  1
) ) )
5917, 58syl 16 . . . . . . . . 9  |-  ( ph  ->  F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) ) )
60 fco 5741 . . . . . . . . 9  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> C  /\  F : ( M ... ( N  +  1 ) ) --> ( M ... ( N  +  1 ) ) )  ->  ( G  o.  F ) : ( M ... ( N  +  1
) ) --> C )
611, 59, 60syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( G  o.  F
) : ( M ... ( N  + 
1 ) ) --> C )
62 fss 5739 . . . . . . . 8  |-  ( ( ( G  o.  F
) : ( M ... ( N  + 
1 ) ) --> C  /\  C  C_  S
)  ->  ( G  o.  F ) : ( M ... ( N  +  1 ) ) --> S )
6361, 16, 62syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( G  o.  F
) : ( M ... ( N  + 
1 ) ) --> S )
6463ffvelrnda 6021 . . . . . 6  |-  ( (
ph  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  x )  e.  S
)
6564adantlr 714 . . . . 5  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  (
( G  o.  F
) `  x )  e.  S )
6650, 51, 55, 57, 65seqsplit 12108 . . . 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 ) ) ) )
67 elfzp12 11757 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( K  e.  ( M ... N
)  <->  ( K  =  M  \/  K  e.  ( ( M  + 
1 ) ... N
) ) ) )
6867biimpa 484 . . . . . 6  |-  ( ( N  e.  ( ZZ>= `  M )  /\  K  e.  ( M ... N
) )  ->  ( K  =  M  \/  K  e.  ( ( M  +  1 ) ... N ) ) )
6915, 68sylan 471 . . . . 5  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( K  =  M  \/  K  e.  ( ( M  + 
1 ) ... N
) ) )
70 seqeq1 12078 . . . . . . . . . . 11  |-  ( K  =  M  ->  seq K (  .+  , 
( G  o.  F
) )  =  seq M (  .+  , 
( G  o.  F
) ) )
7170eqcomd 2475 . . . . . . . . . 10  |-  ( K  =  M  ->  seq M (  .+  , 
( G  o.  F
) )  =  seq K (  .+  , 
( G  o.  F
) ) )
7271fveq1d 5868 . . . . . . . . 9  |-  ( K  =  M  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  K
)  =  (  seq K (  .+  , 
( G  o.  F
) ) `  K
) )
73 f1ocnv 5828 . . . . . . . . . . . . 13  |-  ( F : ( M ... ( N  +  1
) ) -1-1-onto-> ( M ... ( N  +  1 ) )  ->  `' F : ( M ... ( N  +  1
) ) -1-1-onto-> ( M ... ( N  +  1 ) ) )
74 f1of 5816 . . . . . . . . . . . . 13  |-  ( `' F : ( M ... ( N  + 
1 ) ) -1-1-onto-> ( M ... ( N  + 
1 ) )  ->  `' F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) ) )
7517, 73, 743syl 20 . . . . . . . . . . . 12  |-  ( ph  ->  `' F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) ) )
76 peano2uz 11134 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( N  +  1 )  e.  ( ZZ>= `  M )
)
77 eluzfz2 11694 . . . . . . . . . . . . 13  |-  ( ( N  +  1 )  e.  ( ZZ>= `  M
)  ->  ( N  +  1 )  e.  ( M ... ( N  +  1 ) ) )
7815, 76, 773syl 20 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  +  1 )  e.  ( M ... ( N  + 
1 ) ) )
7975, 78ffvelrnd 6022 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F `  ( N  +  1
) )  e.  ( M ... ( N  +  1 ) ) )
8019, 79syl5eqel 2559 . . . . . . . . . 10  |-  ( ph  ->  K  e.  ( M ... ( N  + 
1 ) ) )
81 elfzelz 11688 . . . . . . . . . 10  |-  ( K  e.  ( M ... ( N  +  1
) )  ->  K  e.  ZZ )
82 seq1 12088 . . . . . . . . . 10  |-  ( K  e.  ZZ  ->  (  seq K (  .+  , 
( G  o.  F
) ) `  K
)  =  ( ( G  o.  F ) `
 K ) )
8380, 81, 823syl 20 . . . . . . . . 9  |-  ( ph  ->  (  seq K ( 
.+  ,  ( G  o.  F ) ) `
 K )  =  ( ( G  o.  F ) `  K
) )
8472, 83sylan9eqr 2530 . . . . . . . 8  |-  ( (
ph  /\  K  =  M )  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  K
)  =  ( ( G  o.  F ) `
 K ) )
8584oveq1d 6299 . . . . . . 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 ) ) ) )
86 simpr 461 . . . . . . . . 9  |-  ( (
ph  /\  K  =  M )  ->  K  =  M )
87 eluzfz1 11693 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... N ) )
8815, 87syl 16 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ( M ... N ) )
8988adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  K  =  M )  ->  M  e.  ( M ... N
) )
9086, 89eqeltrd 2555 . . . . . . . 8  |-  ( (
ph  /\  K  =  M )  ->  K  e.  ( M ... N
) )
9113adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  (
x  e.  C  /\  y  e.  C )
)  ->  ( x  .+  y )  =  ( y  .+  x ) )
9216adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  C  C_  S
)
9361adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( G  o.  F ) : ( M ... ( N  +  1 ) ) --> C )
9480adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  K  e.  ( M ... ( N  +  1 ) ) )
95 peano2uz 11134 . . . . . . . . . . 11  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K  +  1 )  e.  ( ZZ>= `  M )
)
96 fzss1 11722 . . . . . . . . . . 11  |-  ( ( K  +  1 )  e.  ( ZZ>= `  M
)  ->  ( ( K  +  1 ) ... ( N  + 
1 ) )  C_  ( M ... ( N  +  1 ) ) )
9757, 95, 963syl 20 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( ( K  +  1 ) ... ( N  + 
1 ) )  C_  ( M ... ( N  +  1 ) ) )
9850, 91, 51, 55, 92, 93, 94, 97seqf1olem2a 12113 . . . . . . . . 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 )
) )
99 1zzd 10895 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  1  e.  ZZ )
100 elfzuz 11684 . . . . . . . . . . . . . . . . . 18  |-  ( K  e.  ( M ... ( N  +  1
) )  ->  K  e.  ( ZZ>= `  M )
)
101 fzss1 11722 . . . . . . . . . . . . . . . . . 18  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K ... N )  C_  ( M ... N ) )
10280, 100, 1013syl 20 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( K ... N
)  C_  ( M ... N ) )
103102sselda 3504 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  x  e.  ( M ... N ) )
10422ffvelrnda 6021 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( J `  x )  e.  ( M ... N ) )
105103, 104syldan 470 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( J `  x )  e.  ( M ... N ) )
106 fvres 5880 . . . . . . . . . . . . . . 15  |-  ( ( J `  x )  e.  ( M ... N )  ->  (
( G  |`  ( M ... N ) ) `
 ( J `  x ) )  =  ( G `  ( J `  x )
) )
107105, 106syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( ( G  |`  ( M ... N ) ) `  ( J `  x ) )  =  ( G `
 ( J `  x ) ) )
108 breq1 4450 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  x  ->  (
k  <  K  <->  x  <  K ) )
109 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  x  ->  k  =  x )
110 oveq1 6291 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  x  ->  (
k  +  1 )  =  ( x  + 
1 ) )
111108, 109, 110ifbieq12d 3966 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  x  ->  if ( k  <  K ,  k ,  ( k  +  1 ) )  =  if ( x  <  K ,  x ,  ( x  +  1 ) ) )
112111fveq2d 5870 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  x  ->  ( F `  if (
k  <  K , 
k ,  ( k  +  1 ) ) )  =  ( F `
 if ( x  <  K ,  x ,  ( x  + 
1 ) ) ) )
113 fvex 5876 . . . . . . . . . . . . . . . . . 18  |-  ( F `
 if ( x  <  K ,  x ,  ( x  + 
1 ) ) )  e.  _V
114112, 18, 113fvmpt 5950 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( M ... N )  ->  ( J `  x )  =  ( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) ) )
115103, 114syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( J `  x )  =  ( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) ) )
116 elfzle1 11689 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( K ... N )  ->  K  <_  x )
117116adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  K  <_  x )
11880, 81syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  K  e.  ZZ )
119118zred 10966 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K  e.  RR )
120119adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  K  e.  RR )
121 elfzelz 11688 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( K ... N )  ->  x  e.  ZZ )
122121adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  x  e.  ZZ )
123122zred 10966 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  x  e.  RR )
124120, 123lenltd 9730 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( K  <_  x  <->  -.  x  <  K ) )
125117, 124mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  -.  x  <  K )
126 iffalse 3948 . . . . . . . . . . . . . . . . . 18  |-  ( -.  x  <  K  ->  if ( x  <  K ,  x ,  ( x  +  1 ) )  =  ( x  + 
1 ) )
127126fveq2d 5870 . . . . . . . . . . . . . . . . 17  |-  ( -.  x  <  K  -> 
( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) )  =  ( F `
 ( x  + 
1 ) ) )
128125, 127syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( F `  if ( x  < 
K ,  x ,  ( x  +  1 ) ) )  =  ( F `  (
x  +  1 ) ) )
129115, 128eqtrd 2508 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( J `  x )  =  ( F `  ( x  +  1 ) ) )
130129fveq2d 5870 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( G `  ( J `  x
) )  =  ( G `  ( F `
 ( x  + 
1 ) ) ) )
131107, 130eqtrd 2508 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( ( G  |`  ( M ... N ) ) `  ( J `  x ) )  =  ( G `
 ( F `  ( x  +  1
) ) ) )
132 fvco3 5944 . . . . . . . . . . . . . . 15  |-  ( ( J : ( M ... N ) --> ( M ... N )  /\  x  e.  ( M ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
13322, 132sylan 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
134103, 133syldan 470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
135 fzp1elp1 11733 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( M ... N )  ->  (
x  +  1 )  e.  ( M ... ( N  +  1
) ) )
136103, 135syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( x  +  1 )  e.  ( M ... ( N  +  1 ) ) )
137 fvco3 5944 . . . . . . . . . . . . . . 15  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  ( x  + 
1 )  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  ( x  +  1 ) )  =  ( G `  ( F `
 ( x  + 
1 ) ) ) )
13859, 137sylan 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  +  1 )  e.  ( M ... ( N  +  1 ) ) )  ->  (
( G  o.  F
) `  ( x  +  1 ) )  =  ( G `  ( F `  ( x  +  1 ) ) ) )
139136, 138syldan 470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( ( G  o.  F ) `  ( x  +  1 ) )  =  ( G `  ( F `
 ( x  + 
1 ) ) ) )
140131, 134, 1393eqtr4d 2518 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  o.  F
) `  ( x  +  1 ) ) )
141140adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  x  e.  ( K ... N
) )  ->  (
( ( G  |`  ( M ... N ) )  o.  J ) `
 x )  =  ( ( G  o.  F ) `  (
x  +  1 ) ) )
14253, 99, 141seqshft2 12101 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  (  seq K (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  =  (  seq ( K  +  1 ) (  .+  ,  ( G  o.  F ) ) `  ( N  +  1 ) ) )
143 fvco3 5944 . . . . . . . . . . . . 13  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  K  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  K )  =  ( G `  ( F `
 K ) ) )
14459, 80, 143syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( G  o.  F ) `  K
)  =  ( G `
 ( F `  K ) ) )
14519fveq2i 5869 . . . . . . . . . . . . . 14  |-  ( F `
 K )  =  ( F `  ( `' F `  ( N  +  1 ) ) )
146 f1ocnvfv2 6171 . . . . . . . . . . . . . . 15  |-  ( ( F : ( M ... ( N  + 
1 ) ) -1-1-onto-> ( M ... ( N  + 
1 ) )  /\  ( N  +  1
)  e.  ( M ... ( N  + 
1 ) ) )  ->  ( F `  ( `' F `  ( N  +  1 ) ) )  =  ( N  +  1 ) )
14717, 78, 146syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  ( `' F `  ( N  +  1 ) ) )  =  ( N  +  1 ) )
148145, 147syl5eq 2520 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F `  K
)  =  ( N  +  1 ) )
149148fveq2d 5870 . . . . . . . . . . . 12  |-  ( ph  ->  ( G `  ( F `  K )
)  =  ( G `
 ( N  + 
1 ) ) )
150144, 149eqtr2d 2509 . . . . . . . . . . 11  |-  ( ph  ->  ( G `  ( N  +  1 ) )  =  ( ( G  o.  F ) `
 K ) )
151150adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  ( G `  ( N  +  1 ) )  =  ( ( G  o.  F
) `  K )
)
152142, 151oveq12d 6302 . . . . . . . . 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 ) ) )
15398, 152eqtr4d 2511 . . . . . . . 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 ) ) ) )
15490, 153syldan 470 . . . . . . 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 ) ) ) )
15586seqeq1d 12081 . . . . . . . . 9  |-  ( (
ph  /\  K  =  M )  ->  seq K (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) )  =  seq M
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) )
156155fveq1d 5868 . . . . . . . 8  |-  ( (
ph  /\  K  =  M )  ->  (  seq K (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  =  (  seq M
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) `
 N ) )
157156oveq1d 6299 . . . . . . 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 ) ) ) )
15885, 154, 1573eqtrd 2512 . . . . . 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 ) ) ) )
159 eluzel2 11087 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
16015, 159syl 16 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ZZ )
161 elfzuz 11684 . . . . . . . . . . 11  |-  ( K  e.  ( ( M  +  1 ) ... N )  ->  K  e.  ( ZZ>= `  ( M  +  1 ) ) )
162 eluzp1m1 11105 . . . . . . . . . . 11  |-  ( ( M  e.  ZZ  /\  K  e.  ( ZZ>= `  ( M  +  1
) ) )  -> 
( K  -  1 )  e.  ( ZZ>= `  M ) )
163160, 161, 162syl2an 477 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  ( K  -  1 )  e.  ( ZZ>= `  M
) )
164 eluzelz 11091 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
16515, 164syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  ZZ )
166165zcnd 10967 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  CC )
167 ax-1cn 9550 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
168 pncan 9826 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
169166, 167, 168sylancl 662 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  N )
170 peano2zm 10906 . . . . . . . . . . . . . . . . . . . 20  |-  ( K  e.  ZZ  ->  ( K  -  1 )  e.  ZZ )
17180, 81, 1703syl 20 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( K  -  1 )  e.  ZZ )
172 elfzuz3 11685 . . . . . . . . . . . . . . . . . . . . 21  |-  ( K  e.  ( M ... ( N  +  1
) )  ->  ( N  +  1 )  e.  ( ZZ>= `  K
) )
17380, 172syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= `  K ) )
174118zcnd 10967 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  K  e.  CC )
175 npcan 9829 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( K  e.  CC  /\  1  e.  CC )  ->  ( ( K  - 
1 )  +  1 )  =  K )
176174, 167, 175sylancl 662 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( K  - 
1 )  +  1 )  =  K )
177176fveq2d 5870 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ZZ>= `  ( ( K  -  1 )  +  1 ) )  =  ( ZZ>= `  K
) )
178173, 177eleqtrrd 2558 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= `  ( ( K  - 
1 )  +  1 ) ) )
179 eluzp1m1 11105 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( K  -  1 )  e.  ZZ  /\  ( N  +  1
)  e.  ( ZZ>= `  ( ( K  - 
1 )  +  1 ) ) )  -> 
( ( N  + 
1 )  -  1 )  e.  ( ZZ>= `  ( K  -  1
) ) )
180171, 178, 179syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  e.  ( ZZ>= `  ( K  -  1
) ) )
181169, 180eqeltrrd 2556 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  ( ZZ>= `  ( K  -  1
) ) )
182 fzss2 11723 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  ( K  -  1 ) )  ->  ( M ... ( K  -  1 ) )  C_  ( M ... N ) )
183181, 182syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( M ... ( K  -  1 ) )  C_  ( M ... N ) )
184183sselda 3504 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  x  e.  ( M ... N ) )
185184, 104syldan 470 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  x )  e.  ( M ... N ) )
186185, 106syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( ( G  |`  ( M ... N ) ) `  ( J `  x ) )  =  ( G `
 ( J `  x ) ) )
187184, 114syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  x )  =  ( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) ) )
188 elfzm11 11749 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  e.  ZZ  /\  K  e.  ZZ )  ->  ( x  e.  ( M ... ( K  -  1 ) )  <-> 
( x  e.  ZZ  /\  M  <_  x  /\  x  <  K ) ) )
189160, 118, 188syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( x  e.  ( M ... ( K  -  1 ) )  <-> 
( x  e.  ZZ  /\  M  <_  x  /\  x  <  K ) ) )
190189biimpa 484 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( x  e.  ZZ  /\  M  <_  x  /\  x  <  K
) )
191190simp3d 1010 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  x  <  K )
192 iftrue 3945 . . . . . . . . . . . . . . . . 17  |-  ( x  <  K  ->  if ( x  <  K ,  x ,  ( x  +  1 ) )  =  x )
193192fveq2d 5870 . . . . . . . . . . . . . . . 16  |-  ( x  <  K  ->  ( F `  if (
x  <  K ,  x ,  ( x  +  1 ) ) )  =  ( F `
 x ) )
194191, 193syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( F `  if ( x  < 
K ,  x ,  ( x  +  1 ) ) )  =  ( F `  x
) )
195187, 194eqtrd 2508 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  x )  =  ( F `  x ) )
196195fveq2d 5870 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( J `  x
) )  =  ( G `  ( F `
 x ) ) )
197186, 196eqtr2d 2509 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( F `  x
) )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
198 peano2uz 11134 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  ( K  -  1 ) )  ->  ( N  +  1 )  e.  ( ZZ>= `  ( K  -  1 ) ) )
199 fzss2 11723 . . . . . . . . . . . . . . 15  |-  ( ( N  +  1 )  e.  ( ZZ>= `  ( K  -  1 ) )  ->  ( M ... ( K  -  1 ) )  C_  ( M ... ( N  + 
1 ) ) )
200181, 198, 1993syl 20 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M ... ( K  -  1 ) )  C_  ( M ... ( N  +  1 ) ) )
201200sselda 3504 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  x  e.  ( M ... ( N  +  1 ) ) )
202 fvco3 5944 . . . . . . . . . . . . . 14  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  x )  =  ( G `  ( F `
 x ) ) )
20359, 202sylan 471 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  x )  =  ( G `  ( F `
 x ) ) )
204201, 203syldan 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( ( G  o.  F ) `  x )  =  ( G `  ( F `
 x ) ) )
205184, 133syldan 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  =  ( ( G  |`  ( M ... N ) ) `
 ( J `  x ) ) )
206197, 204, 2053eqtr4d 2518 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( ( G  o.  F ) `  x )  =  ( ( ( G  |`  ( M ... N ) )  o.  J ) `
 x ) )
207206adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  (
( G  o.  F
) `  x )  =  ( ( ( G  |`  ( M ... N ) )  o.  J ) `  x
) )
208163, 207seqfveq 12099 . . . . . . . . 9  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  ( K  -  1 ) )  =  (  seq M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  ( K  -  1 ) ) )
209 fzp1ss 11731 . . . . . . . . . . . 12  |-  ( M  e.  ZZ  ->  (
( M  +  1 ) ... N ) 
C_  ( M ... N ) )
21015, 159, 2093syl 20 . . . . . . . . . . 11  |-  ( ph  ->  ( ( M  + 
1 ) ... N
)  C_  ( M ... N ) )
211210sselda 3504 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  K  e.  ( M ... N
) )
212211, 153syldan 470 . . . . . . . . 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 ) ) ) )
213208, 212oveq12d 6302 . . . . . . . 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 ) ) ) ) )
214201, 64syldan 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( ( G  o.  F ) `  x )  e.  S
)
215214adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  (
( G  o.  F
) `  x )  e.  S )
21612adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  .+  y )  e.  S
)
217163, 215, 216seqcl 12095 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  ( K  -  1 ) )  e.  S )
21861, 80ffvelrnd 6022 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( G  o.  F ) `  K
)  e.  C )
21916, 218sseldd 3505 . . . . . . . . . . 11  |-  ( ph  ->  ( ( G  o.  F ) `  K
)  e.  S )
220219adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (
( G  o.  F
) `  K )  e.  S )
22197sselda 3504 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  x  e.  ( ( K  + 
1 ) ... ( N  +  1 ) ) )  ->  x  e.  ( M ... ( N  +  1 ) ) )
222221, 65syldan 470 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  e.  ( M ... N
) )  /\  x  e.  ( ( K  + 
1 ) ... ( N  +  1 ) ) )  ->  (
( G  o.  F
) `  x )  e.  S )
22355, 222, 50seqcl 12095 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  (  seq ( K  +  1
) (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  e.  S )
224211, 223syldan 470 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq ( K  +  1 ) (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  e.  S )
225217, 220, 2243jca 1176 . . . . . . . . 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
) )
22614caovassg 6457 . . . . . . . . 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
) ) ) ) )
227225, 226syldan 470 . . . . . . . 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
) ) ) ) )
228 fss 5739 . . . . . . . . . . . . . . . . 17  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> C  /\  C  C_  S
)  ->  G :
( M ... ( N  +  1 ) ) --> S )
2291, 16, 228syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G : ( M ... ( N  + 
1 ) ) --> S )
230 fssres 5751 . . . . . . . . . . . . . . . 16  |-  ( ( G : ( M ... ( N  + 
1 ) ) --> S  /\  ( M ... N )  C_  ( M ... ( N  + 
1 ) ) )  ->  ( G  |`  ( M ... N ) ) : ( M ... N ) --> S )
231229, 4, 230sylancl 662 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G  |`  ( M ... N ) ) : ( M ... N ) --> S )
232 fco 5741 . . . . . . . . . . . . . . 15  |-  ( ( ( G  |`  ( M ... N ) ) : ( M ... N ) --> S  /\  J : ( M ... N ) --> ( M ... N ) )  ->  ( ( G  |`  ( M ... N
) )  o.  J
) : ( M ... N ) --> S )
233231, 22, 232syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G  |`  ( M ... N ) )  o.  J ) : ( M ... N ) --> S )
234233ffvelrnda 6021 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  e.  S
)
235184, 234syldan 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  e.  S
)
236235adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( M ... ( K  -  1 ) ) )  ->  (
( ( G  |`  ( M ... N ) )  o.  J ) `
 x )  e.  S )
237163, 236, 216seqcl 12095 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  ( K  -  1 ) )  e.  S )
238 elfzuz3 11685 . . . . . . . . . . . 12  |-  ( K  e.  ( ( M  +  1 ) ... N )  ->  N  e.  ( ZZ>= `  K )
)
239238adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  N  e.  ( ZZ>= `  K )
)
240103, 234syldan 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( K ... N ) )  ->  ( (
( G  |`  ( M ... N ) )  o.  J ) `  x )  e.  S
)
241240adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( K ... N
) )  ->  (
( ( G  |`  ( M ... N ) )  o.  J ) `
 x )  e.  S )
242239, 241, 216seqcl 12095 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq K (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N )  e.  S )
243229, 78ffvelrnd 6022 . . . . . . . . . . 11  |-  ( ph  ->  ( G `  ( N  +  1 ) )  e.  S )
244243adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  ( G `  ( N  +  1 ) )  e.  S )
245237, 242, 2443jca 1176 . . . . . . . . 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 ) )
24614caovassg 6457 . . . . . . . . 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
) ) ) ) )
247245, 246syldan 470 . . . . . . . 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 ) ) ) ) )
248213, 227, 2473eqtr4d 2518 . . . . . . 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
) ) ) )
249 seqm1 12092 . . . . . . . . 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
) ) )
250160, 161, 249syl2an 477 . . . . . . . 8  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  K
)  =  ( (  seq M (  .+  ,  ( G  o.  F ) ) `  ( K  -  1
) )  .+  (
( G  o.  F
) `  K )
) )
251250oveq1d 6299 . . . . . . 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
) ) ) )
25214adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  (
x  e.  S  /\  y  e.  S  /\  z  e.  S )
)  ->  ( (
x  .+  y )  .+  z )  =  ( x  .+  ( y 
.+  z ) ) )
253 elfzelz 11688 . . . . . . . . . . . . . . 15  |-  ( K  e.  ( ( M  +  1 ) ... N )  ->  K  e.  ZZ )
254253adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  K  e.  ZZ )
255254zcnd 10967 . . . . . . . . . . . . 13  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  K  e.  CC )
256255, 167, 175sylancl 662 . . . . . . . . . . . 12  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  (
( K  -  1 )  +  1 )  =  K )
257256fveq2d 5870 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  ( ZZ>=
`  ( ( K  -  1 )  +  1 ) )  =  ( ZZ>= `  K )
)
258239, 257eleqtrrd 2558 . . . . . . . . . 10  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  N  e.  ( ZZ>= `  ( ( K  -  1 )  +  1 ) ) )
259234adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  /\  x  e.  ( M ... N
) )  ->  (
( ( G  |`  ( M ... N ) )  o.  J ) `
 x )  e.  S )
260216, 252, 258, 163, 259seqsplit 12108 . . . . . . . . 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 ) ) )
261256seqeq1d 12081 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( M  + 
1 ) ... N
) )  ->  seq ( ( K  - 
1 )  +  1 ) (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) )  =  seq K
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) )
262261fveq1d 5868 . . . . . . . . . 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 ) )
263262oveq2d 6300 . . . . . . . . 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 ) ) )
264260, 263eqtrd 2508 . . . . . . . 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 ) ) )
265264oveq1d 6299 . . . . . . 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
) ) ) )
266248, 251, 2653eqtr4d 2518 . . . . . 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 ) ) ) )
267158, 266jaodan 783 . . . . 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 ) ) ) )
26869, 267syldan 470 . . . 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 ) ) ) )
26966, 268eqtrd 2508 . . 3  |-  ( (
ph  /\  K  e.  ( M ... N ) )  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  =  ( (  seq M (  .+  ,  ( ( G  |`  ( M ... N
) )  o.  J
) ) `  N
)  .+  ( G `  ( N  +  1 ) ) ) )
27015adantr 465 . . . . 5  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  N  e.  ( ZZ>= `  M )
)
271 seqp1 12090 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  =  ( (  seq M (  .+  ,  ( G  o.  F ) ) `  N )  .+  (
( G  o.  F
) `  ( N  +  1 ) ) ) )
272270, 271syl 16 . . . 4  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  =  ( (  seq M (  .+  ,  ( G  o.  F ) ) `  N )  .+  (
( G  o.  F
) `  ( N  +  1 ) ) ) )
273114adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( J `  x
)  =  ( F `
 if ( x  <  K ,  x ,  ( x  + 
1 ) ) ) )
274 elfzelz 11688 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( M ... N )  ->  x  e.  ZZ )
275274zred 10966 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( M ... N )  ->  x  e.  RR )
276275adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  x  e.  RR )
277165zred 10966 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  RR )
278277adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  N  e.  RR )
279 peano2re 9752 . . . . . . . . . . . . . . 15  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
280278, 279syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( N  +  1 )  e.  RR )
281 elfzle2 11690 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( M ... N )  ->  x  <_  N )
282281adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  x  <_  N )
283278ltp1d 10476 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  N  <  ( N  +  1 ) )
284276, 278, 280, 282, 283lelttrd 9739 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  x  <  ( N  +  1 ) )
285284adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  x  <  ( N  + 
1 ) )
286 simplr 754 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  K  =  ( N  +  1 ) )
287285, 286breqtrrd 4473 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  x  <  K )
288287, 193syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( F `  if ( x  <  K ,  x ,  ( x  +  1 ) ) )  =  ( F `
 x ) )
289273, 288eqtrd 2508 . . . . . . . . 9  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( J `  x
)  =  ( F `
 x ) )
290289fveq2d 5870 . . . . . . . 8  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( G  |`  ( M ... N ) ) `  ( J `
 x ) )  =  ( ( G  |`  ( M ... N
) ) `  ( F `  x )
) )
291275adantl 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  x  e.  RR )
292291, 287gtned 9719 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  K  =/=  x )
29359ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  F : ( M ... ( N  +  1
) ) --> ( M ... ( N  + 
1 ) ) )
294 fzelp1 11732 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( M ... N )  ->  x  e.  ( M ... ( N  +  1 ) ) )
295294adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  x  e.  ( M ... ( N  +  1 ) ) )
296293, 295ffvelrnd 6022 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( F `  x
)  e.  ( M ... ( N  + 
1 ) ) )
29715ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  N  e.  ( ZZ>= `  M ) )
298 elfzp1 11730 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ( F `  x )  e.  ( M ... ( N  +  1 ) )  <->  ( ( F `
 x )  e.  ( M ... N
)  \/  ( F `
 x )  =  ( N  +  1 ) ) ) )
299297, 298syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( F `  x )  e.  ( M ... ( N  +  1 ) )  <-> 
( ( F `  x )  e.  ( M ... N )  \/  ( F `  x )  =  ( N  +  1 ) ) ) )
300296, 299mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( F `  x )  e.  ( M ... N )  \/  ( F `  x )  =  ( N  +  1 ) ) )
301300ord 377 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( -.  ( F `
 x )  e.  ( M ... N
)  ->  ( F `  x )  =  ( N  +  1 ) ) )
30217ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  ->  F : ( M ... ( N  +  1
) ) -1-1-onto-> ( M ... ( N  +  1 ) ) )
303 f1ocnvfv 6172 . . . . . . . . . . . . . 14  |-  ( ( F : ( M ... ( N  + 
1 ) ) -1-1-onto-> ( M ... ( N  + 
1 ) )  /\  x  e.  ( M ... ( N  +  1 ) ) )  -> 
( ( F `  x )  =  ( N  +  1 )  ->  ( `' F `  ( N  +  1 ) )  =  x ) )
304302, 295, 303syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( F `  x )  =  ( N  +  1 )  ->  ( `' F `  ( N  +  1 ) )  =  x ) )
30519eqeq1i 2474 . . . . . . . . . . . . 13  |-  ( K  =  x  <->  ( `' F `  ( N  +  1 ) )  =  x )
306304, 305syl6ibr 227 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( F `  x )  =  ( N  +  1 )  ->  K  =  x ) )
307301, 306syld 44 . . . . . . . . . . 11  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( -.  ( F `
 x )  e.  ( M ... N
)  ->  K  =  x ) )
308307necon1ad 2683 . . . . . . . . . 10  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( K  =/=  x  ->  ( F `  x
)  e.  ( M ... N ) ) )
309292, 308mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( F `  x
)  e.  ( M ... N ) )
310 fvres 5880 . . . . . . . . 9  |-  ( ( F `  x )  e.  ( M ... N )  ->  (
( G  |`  ( M ... N ) ) `
 ( F `  x ) )  =  ( G `  ( F `  x )
) )
311309, 310syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( G  |`  ( M ... N ) ) `  ( F `
 x ) )  =  ( G `  ( F `  x ) ) )
312290, 311eqtr2d 2509 . . . . . . 7  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( G `  ( F `  x )
)  =  ( ( G  |`  ( M ... N ) ) `  ( J `  x ) ) )
31359, 294, 202syl2an 477 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( ( G  o.  F ) `  x )  =  ( G `  ( F `
 x ) ) )
314313adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( G  o.  F ) `  x
)  =  ( G `
 ( F `  x ) ) )
315133adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( ( G  |`  ( M ... N
) )  o.  J
) `  x )  =  ( ( G  |`  ( M ... N
) ) `  ( J `  x )
) )
316312, 314, 3153eqtr4d 2518 . . . . . 6  |-  ( ( ( ph  /\  K  =  ( N  + 
1 ) )  /\  x  e.  ( M ... N ) )  -> 
( ( G  o.  F ) `  x
)  =  ( ( ( G  |`  ( M ... N ) )  o.  J ) `  x ) )
317270, 316seqfveq 12099 . . . . 5  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  N
)  =  (  seq M (  .+  , 
( ( G  |`  ( M ... N ) )  o.  J ) ) `  N ) )
318 fvco3 5944 . . . . . . . 8  |-  ( ( F : ( M ... ( N  + 
1 ) ) --> ( M ... ( N  +  1 ) )  /\  ( N  + 
1 )  e.  ( M ... ( N  +  1 ) ) )  ->  ( ( G  o.  F ) `  ( N  +  1 ) )  =  ( G `  ( F `
 ( N  + 
1 ) ) ) )
31959, 78, 318syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( G  o.  F ) `  ( N  +  1 ) )  =  ( G `
 ( F `  ( N  +  1
) ) ) )
320319adantr 465 . . . . . 6  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (
( G  o.  F
) `  ( N  +  1 ) )  =  ( G `  ( F `  ( N  +  1 ) ) ) )
321 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  K  =  ( N  + 
1 ) )
32219, 321syl5eqr 2522 . . . . . . . . 9  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( `' F `  ( N  +  1 ) )  =  ( N  + 
1 ) )
323322fveq2d 5870 . . . . . . . 8  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( F `  ( `' F `  ( N  +  1 ) ) )  =  ( F `
 ( N  + 
1 ) ) )
324147adantr 465 . . . . . . . 8  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( F `  ( `' F `  ( N  +  1 ) ) )  =  ( N  +  1 ) )
325323, 324eqtr3d 2510 . . . . . . 7  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( F `  ( N  +  1 ) )  =  ( N  + 
1 ) )
326325fveq2d 5870 . . . . . 6  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  ( G `  ( F `  ( N  +  1 ) ) )  =  ( G `  ( N  +  1 ) ) )
327320, 326eqtrd 2508 . . . . 5  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (
( G  o.  F
) `  ( N  +  1 ) )  =  ( G `  ( N  +  1
) ) )
328317, 327oveq12d 6302 . . . 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 ) ) ) )
329272, 328eqtrd 2508 . . 3  |-  ( (
ph  /\  K  =  ( N  +  1
) )  ->  (  seq M (  .+  , 
( G  o.  F
) ) `  ( N  +  1 ) )  =  ( (  seq M (  .+  ,  ( ( G  |`  ( M ... N
) )  o.  J
) ) `  N
)  .+  ( G `  ( N  +  1 ) ) ) )
330 elfzp1 11730 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( K  e.  ( M ... ( N  +  1 ) )  <->  ( K  e.  ( M ... N
)  \/  K  =  ( N  +  1 ) ) ) )
33115, 330syl 16 . . . 4  |-  ( ph  ->  ( K  e.  ( M ... ( N  +  1 ) )  <-> 
( K  e.  ( M ... N )  \/  K  =  ( N  +  1 ) ) ) )
33280, 331mpbid 210 . . 3  |-  ( ph  ->  ( K  e.  ( M ... N )  \/  K  =  ( N  +  1 ) ) )
333269, 329, 332mpjaodan 784 . 2  |-  ( ph  ->  (  seq M ( 
.+  ,  ( G  o.  F ) ) `
 ( N  + 
1 ) )  =  ( (  seq M
(  .+  ,  (
( G  |`  ( M ... N ) )  o.  J ) ) `
 N )  .+  ( G `  ( N  +  1 ) ) ) )
334 seqp1 12090 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  (  seq M (  .+  ,  G ) `  ( N  +  1 ) )  =  ( (  seq M (  .+  ,  G ) `  N
)  .+  ( G `  ( N  +  1 ) ) ) )
33515, 334syl 16 . 2  |-  ( ph  ->  (  seq M ( 
.+  ,  G ) `
 ( N  + 
1 ) )  =  ( (  seq M
(  .+  ,  G
) `  N )  .+  ( G `  ( N  +  1 ) ) ) )
33649, 333, 3353eqtr4d 2518 1  |-  ( ph  ->  (  seq M ( 
.+  ,  ( G  o.  F ) ) `
 ( N  + 
1 ) )  =  (  seq M ( 
.+  ,  G ) `
 ( N  + 
1 ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 973   A.wal 1377    = wceq 1379    e. wcel 1767    =/= wne 2662   _Vcvv 3113    C_ wss 3476   ifcif 3939   class class class wbr 4447    |-> cmpt 4505   `'ccnv 4998    |` cres 5001    o. ccom 5003    Fn wfn 5583   -->wf 5584   -1-1-onto->wf1o 5587   ` cfv 5588  (class class class)co 6284   Fincfn 7516   CCcc 9490   RRcr 9491   1c1 9493    + caddc 9495    < clt 9628    <_ cle 9629    - cmin 9805   ZZcz 10864   ZZ>=cuz 11082   ...cfz 11672    seqcseq 12075
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-n0 10796  df-z 10865  df-uz 11083  df-fz 11673  df-fzo 11793  df-seq 12076
This theorem is referenced by:  seqf1o  12116
  Copyright terms: Public domain W3C validator