ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  seq3f1olemqsum Unicode version

Theorem seq3f1olemqsum 9925
Description: Lemma for seq3f1o 9929. 
Q gives the same sum as 
J. (Contributed by Jim Kingdon, 21-Aug-2022.)
Hypotheses
Ref Expression
iseqf1o.1  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  e.  S )
iseqf1o.2  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  =  ( y 
.+  x ) )
iseqf1o.3  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S ) )  -> 
( ( x  .+  y )  .+  z
)  =  ( x 
.+  ( y  .+  z ) ) )
iseqf1o.4  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
iseqf1o.6  |-  ( ph  ->  F : ( M ... N ) -1-1-onto-> ( M ... N ) )
iseqf1o.7  |-  ( (
ph  /\  x  e.  ( ZZ>= `  M )
)  ->  ( G `  x )  e.  S
)
iseqf1olemstep.k  |-  ( ph  ->  K  e.  ( M ... N ) )
iseqf1olemstep.j  |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )
iseqf1olemstep.const  |-  ( ph  ->  A. x  e.  ( M..^ K ) ( J `  x )  =  x )
iseqf1olemnk  |-  ( ph  ->  K  =/=  ( `' J `  K ) )
iseqf1olemqres.q  |-  Q  =  ( u  e.  ( M ... N ) 
|->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `  u
) ) )
iseqf1olemqsumk.p  |-  P  =  ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )
Assertion
Ref Expression
seq3f1olemqsum  |-  ( ph  ->  (  seq M ( 
.+  ,  [_ J  /  f ]_ P
) `  N )  =  (  seq M ( 
.+  ,  [_ Q  /  f ]_ P
) `  N )
)
Distinct variable groups:    u, J    u, K, x    u, M, x   
u, N    x, J    x, Q    ph, x, y, z    ph, u    x,  .+ , y,
z    x, S, y, z   
f, M, y, z   
f, N, x, y, z    y, K, z   
f, G, x    f, J, y, z    x, P, y, z    Q, f, y, z
Allowed substitution hints:    ph( f)    P( u, f)    .+ ( u, f)    Q( u)    S( u, f)    F( x, y, z, u, f)    G( y, z, u)    K( f)

Proof of Theorem seq3f1olemqsum
Dummy variables  b  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iseqf1olemstep.k . . . . . . . 8  |-  ( ph  ->  K  e.  ( M ... N ) )
2 elfzel1 9437 . . . . . . . 8  |-  ( K  e.  ( M ... N )  ->  M  e.  ZZ )
31, 2syl 14 . . . . . . 7  |-  ( ph  ->  M  e.  ZZ )
43adantr 270 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  M  e.  ZZ )
5 elfzelz 9438 . . . . . . . . 9  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )
61, 5syl 14 . . . . . . . 8  |-  ( ph  ->  K  e.  ZZ )
76adantr 270 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  K  e.  ZZ )
8 peano2zm 8786 . . . . . . 7  |-  ( K  e.  ZZ  ->  ( K  -  1 )  e.  ZZ )
97, 8syl 14 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  ( K  -  1 )  e.  ZZ )
10 simpr 108 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  M  <  K )
11 zltlem1 8805 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  K  e.  ZZ )  ->  ( M  <  K  <->  M  <_  ( K  - 
1 ) ) )
124, 7, 11syl2anc 403 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  ( M  <  K  <->  M  <_  ( K  -  1 ) ) )
1310, 12mpbid 145 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  M  <_  ( K  -  1 ) )
14 eluz2 9023 . . . . . 6  |-  ( ( K  -  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( K  -  1 )  e.  ZZ  /\  M  <_ 
( K  -  1 ) ) )
154, 9, 13, 14syl3anbrc 1127 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  ( K  -  1 )  e.  ( ZZ>= `  M )
)
163ad2antrr 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  M  e.  ZZ )
17 elfzel2 9436 . . . . . . . . . . . 12  |-  ( K  e.  ( M ... N )  ->  N  e.  ZZ )
181, 17syl 14 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ZZ )
1918ad2antrr 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  N  e.  ZZ )
20 elfzelz 9438 . . . . . . . . . . 11  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  e.  ZZ )
2120adantl 271 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ZZ )
22 elfzle1 9439 . . . . . . . . . . 11  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  M  <_  b )
2322adantl 271 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  M  <_  b )
2421zred 8866 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  RR )
256ad2antrr 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  e.  ZZ )
2625zred 8866 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  e.  RR )
2719zred 8866 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  N  e.  RR )
28 peano2rem 7747 . . . . . . . . . . . . 13  |-  ( K  e.  RR  ->  ( K  -  1 )  e.  RR )
2926, 28syl 14 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( K  -  1 )  e.  RR )
30 elfzle2 9440 . . . . . . . . . . . . 13  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  <_  ( K  -  1 ) )
3130adantl 271 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  ( K  -  1 ) )
3226lem1d 8392 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( K  -  1 )  <_  K )
3324, 29, 26, 31, 32letrd 7605 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  K )
34 elfzle2 9440 . . . . . . . . . . . . 13  |-  ( K  e.  ( M ... N )  ->  K  <_  N )
351, 34syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  K  <_  N )
3635ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  <_  N )
3724, 26, 27, 33, 36letrd 7605 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  N )
38 elfz4 9431 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  b  e.  ZZ )  /\  ( M  <_  b  /\  b  <_  N ) )  ->  b  e.  ( M ... N ) )
3916, 19, 21, 23, 37, 38syl32anc 1182 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ( M ... N
) )
40 elfzel1 9437 . . . . . . . . . . . . . 14  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  e.  ZZ )
4140zred 8866 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  e.  RR )
42 elfzelz 9438 . . . . . . . . . . . . . 14  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  b  e.  ZZ )
4342zred 8866 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  b  e.  RR )
44 elfzle1 9439 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  <_  b )
4541, 43, 44lensymd 7603 . . . . . . . . . . . 12  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  -.  b  <  K )
46 zltlem1 8805 . . . . . . . . . . . . . 14  |-  ( ( b  e.  ZZ  /\  K  e.  ZZ )  ->  ( b  <  K  <->  b  <_  ( K  - 
1 ) ) )
4721, 25, 46syl2anc 403 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  (
b  <  K  <->  b  <_  ( K  -  1 ) ) )
4831, 47mpbird 165 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <  K )
4945, 48nsyl3 591 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  -.  b  e.  ( K ... ( `' J `  K ) ) )
5049iffalsed 3403 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  e.  ( K ... ( `' J `  K ) ) ,  if ( b  =  K ,  K ,  ( J `  ( b  -  1 ) ) ) ,  ( J `  b
) )  =  ( J `  b ) )
51 iseqf1olemstep.j . . . . . . . . . . . . 13  |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )
52 f1of 5253 . . . . . . . . . . . . 13  |-  ( J : ( M ... N ) -1-1-onto-> ( M ... N
)  ->  J :
( M ... N
) --> ( M ... N ) )
5351, 52syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  J : ( M ... N ) --> ( M ... N ) )
5453ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  J : ( M ... N ) --> ( M ... N ) )
5554, 39ffvelrnd 5435 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  b )  e.  ( M ... N
) )
5650, 55eqeltrd 2164 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  e.  ( K ... ( `' J `  K ) ) ,  if ( b  =  K ,  K ,  ( J `  ( b  -  1 ) ) ) ,  ( J `  b
) )  e.  ( M ... N ) )
57 eleq1w 2148 . . . . . . . . . . 11  |-  ( u  =  b  ->  (
u  e.  ( K ... ( `' J `  K ) )  <->  b  e.  ( K ... ( `' J `  K ) ) ) )
58 eqeq1 2094 . . . . . . . . . . . 12  |-  ( u  =  b  ->  (
u  =  K  <->  b  =  K ) )
59 fvoveq1 5675 . . . . . . . . . . . 12  |-  ( u  =  b  ->  ( J `  ( u  -  1 ) )  =  ( J `  ( b  -  1 ) ) )
6058, 59ifbieq2d 3415 . . . . . . . . . . 11  |-  ( u  =  b  ->  if ( u  =  K ,  K ,  ( J `
 ( u  - 
1 ) ) )  =  if ( b  =  K ,  K ,  ( J `  ( b  -  1 ) ) ) )
61 fveq2 5305 . . . . . . . . . . 11  |-  ( u  =  b  ->  ( J `  u )  =  ( J `  b ) )
6257, 60, 61ifbieq12d 3417 . . . . . . . . . 10  |-  ( u  =  b  ->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K , 
( J `  (
u  -  1 ) ) ) ,  ( J `  u ) )  =  if ( b  e.  ( K ... ( `' J `  K ) ) ,  if ( b  =  K ,  K , 
( J `  (
b  -  1 ) ) ) ,  ( J `  b ) ) )
63 iseqf1olemqres.q . . . . . . . . . 10  |-  Q  =  ( u  e.  ( M ... N ) 
|->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `  u
) ) )
6462, 63fvmptg 5380 . . . . . . . . 9  |-  ( ( b  e.  ( M ... N )  /\  if ( b  e.  ( K ... ( `' J `  K ) ) ,  if ( b  =  K ,  K ,  ( J `  ( b  -  1 ) ) ) ,  ( J `  b
) )  e.  ( M ... N ) )  ->  ( Q `  b )  =  if ( b  e.  ( K ... ( `' J `  K ) ) ,  if ( b  =  K ,  K ,  ( J `  ( b  -  1 ) ) ) ,  ( J `  b
) ) )
6539, 56, 64syl2anc 403 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( Q `  b )  =  if ( b  e.  ( K ... ( `' J `  K ) ) ,  if ( b  =  K ,  K ,  ( J `  ( b  -  1 ) ) ) ,  ( J `  b
) ) )
6665, 50eqtrd 2120 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( Q `  b )  =  ( J `  b ) )
6766fveq2d 5309 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( Q `  b ) )  =  ( G `  ( J `  b )
) )
68 iseqf1olemqsumk.p . . . . . . . . . . 11  |-  P  =  ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )
6968csbeq2i 2957 . . . . . . . . . 10  |-  [_ Q  /  f ]_ P  =  [_ Q  /  f ]_ ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )
703, 18fzfigd 9834 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M ... N
)  e.  Fin )
71 mptexg 5522 . . . . . . . . . . . . 13  |-  ( ( M ... N )  e.  Fin  ->  (
u  e.  ( M ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `  u
) ) )  e. 
_V )
7270, 71syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  ( M ... N ) 
|->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `  u
) ) )  e. 
_V )
7363, 72syl5eqel 2174 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  _V )
74 nfcvd 2229 . . . . . . . . . . . 12  |-  ( Q  e.  _V  ->  F/_ f
( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( Q `  x ) ) ,  ( G `
 M ) ) ) )
75 fveq1 5304 . . . . . . . . . . . . . . 15  |-  ( f  =  Q  ->  (
f `  x )  =  ( Q `  x ) )
7675fveq2d 5309 . . . . . . . . . . . . . 14  |-  ( f  =  Q  ->  ( G `  ( f `  x ) )  =  ( G `  ( Q `  x )
) )
7776ifeq1d 3408 . . . . . . . . . . . . 13  |-  ( f  =  Q  ->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) )  =  if ( x  <_  N ,  ( G `  ( Q `
 x ) ) ,  ( G `  M ) ) )
7877mpteq2dv 3929 . . . . . . . . . . . 12  |-  ( f  =  Q  ->  (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) ) )  =  ( x  e.  ( ZZ>= `  M
)  |->  if ( x  <_  N ,  ( G `  ( Q `
 x ) ) ,  ( G `  M ) ) ) )
7974, 78csbiegf 2971 . . . . . . . . . . 11  |-  ( Q  e.  _V  ->  [_ Q  /  f ]_ (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) ) )  =  ( x  e.  ( ZZ>= `  M
)  |->  if ( x  <_  N ,  ( G `  ( Q `
 x ) ) ,  ( G `  M ) ) ) )
8073, 79syl 14 . . . . . . . . . 10  |-  ( ph  ->  [_ Q  /  f ]_ ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )  =  ( x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  ( Q `  x )
) ,  ( G `
 M ) ) ) )
8169, 80syl5eq 2132 . . . . . . . . 9  |-  ( ph  ->  [_ Q  /  f ]_ P  =  (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  ( Q `  x )
) ,  ( G `
 M ) ) ) )
8281ad2antrr 472 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  [_ Q  /  f ]_ P  =  ( x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( Q `  x
) ) ,  ( G `  M ) ) ) )
83 breq1 3848 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  <_  N  <->  b  <_  N ) )
84 2fveq3 5310 . . . . . . . . . 10  |-  ( x  =  b  ->  ( G `  ( Q `  x ) )  =  ( G `  ( Q `  b )
) )
8583, 84ifbieq1d 3413 . . . . . . . . 9  |-  ( x  =  b  ->  if ( x  <_  N , 
( G `  ( Q `  x )
) ,  ( G `
 M ) )  =  if ( b  <_  N ,  ( G `  ( Q `
 b ) ) ,  ( G `  M ) ) )
8685adantl 271 . . . . . . . 8  |-  ( ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  /\  x  =  b )  ->  if ( x  <_  N ,  ( G `  ( Q `  x
) ) ,  ( G `  M ) )  =  if ( b  <_  N , 
( G `  ( Q `  b )
) ,  ( G `
 M ) ) )
87 elfzuz 9434 . . . . . . . . 9  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  e.  ( ZZ>= `  M )
)
8887adantl 271 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ( ZZ>= `  M )
)
8937iftrued 3400 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( Q `  b ) ) ,  ( G `
 M ) )  =  ( G `  ( Q `  b ) ) )
90 fveq2 5305 . . . . . . . . . . 11  |-  ( a  =  ( Q `  b )  ->  ( G `  a )  =  ( G `  ( Q `  b ) ) )
9190eleq1d 2156 . . . . . . . . . 10  |-  ( a  =  ( Q `  b )  ->  (
( G `  a
)  e.  S  <->  ( G `  ( Q `  b
) )  e.  S
) )
92 iseqf1o.7 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ZZ>= `  M )
)  ->  ( G `  x )  e.  S
)
9392ralrimiva 2446 . . . . . . . . . . . 12  |-  ( ph  ->  A. x  e.  (
ZZ>= `  M ) ( G `  x )  e.  S )
94 fveq2 5305 . . . . . . . . . . . . . 14  |-  ( x  =  a  ->  ( G `  x )  =  ( G `  a ) )
9594eleq1d 2156 . . . . . . . . . . . . 13  |-  ( x  =  a  ->  (
( G `  x
)  e.  S  <->  ( G `  a )  e.  S
) )
9695cbvralv 2590 . . . . . . . . . . . 12  |-  ( A. x  e.  ( ZZ>= `  M ) ( G `
 x )  e.  S  <->  A. a  e.  (
ZZ>= `  M ) ( G `  a )  e.  S )
9793, 96sylib 120 . . . . . . . . . . 11  |-  ( ph  ->  A. a  e.  (
ZZ>= `  M ) ( G `  a )  e.  S )
9897ad2antrr 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  A. a  e.  ( ZZ>= `  M )
( G `  a
)  e.  S )
991, 51, 63iseqf1olemqf 9916 . . . . . . . . . . . . 13  |-  ( ph  ->  Q : ( M ... N ) --> ( M ... N ) )
10099ad2antrr 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  Q : ( M ... N ) --> ( M ... N ) )
101100, 39ffvelrnd 5435 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( Q `  b )  e.  ( M ... N
) )
102 elfzuz 9434 . . . . . . . . . . 11  |-  ( ( Q `  b )  e.  ( M ... N )  ->  ( Q `  b )  e.  ( ZZ>= `  M )
)
103101, 102syl 14 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( Q `  b )  e.  ( ZZ>= `  M )
)
10491, 98, 103rspcdva 2727 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( Q `  b ) )  e.  S )
10589, 104eqeltrd 2164 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( Q `  b ) ) ,  ( G `
 M ) )  e.  S )
10682, 86, 88, 105fvmptd 5385 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ Q  /  f ]_ P `  b )  =  if ( b  <_  N ,  ( G `  ( Q `
 b ) ) ,  ( G `  M ) ) )
107106, 89eqtrd 2120 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ Q  /  f ]_ P `  b )  =  ( G `  ( Q `  b ) ) )
10868csbeq2i 2957 . . . . . . . . . 10  |-  [_ J  /  f ]_ P  =  [_ J  /  f ]_ ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )
109 fex 5524 . . . . . . . . . . . 12  |-  ( ( J : ( M ... N ) --> ( M ... N )  /\  ( M ... N )  e.  Fin )  ->  J  e.  _V )
11053, 70, 109syl2anc 403 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  _V )
111 nfcvd 2229 . . . . . . . . . . . 12  |-  ( J  e.  _V  ->  F/_ f
( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( J `  x ) ) ,  ( G `
 M ) ) ) )
112 fveq1 5304 . . . . . . . . . . . . . . 15  |-  ( f  =  J  ->  (
f `  x )  =  ( J `  x ) )
113112fveq2d 5309 . . . . . . . . . . . . . 14  |-  ( f  =  J  ->  ( G `  ( f `  x ) )  =  ( G `  ( J `  x )
) )
114113ifeq1d 3408 . . . . . . . . . . . . 13  |-  ( f  =  J  ->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) )  =  if ( x  <_  N ,  ( G `  ( J `
 x ) ) ,  ( G `  M ) ) )
115114mpteq2dv 3929 . . . . . . . . . . . 12  |-  ( f  =  J  ->  (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) ) )  =  ( x  e.  ( ZZ>= `  M
)  |->  if ( x  <_  N ,  ( G `  ( J `
 x ) ) ,  ( G `  M ) ) ) )
116111, 115csbiegf 2971 . . . . . . . . . . 11  |-  ( J  e.  _V  ->  [_ J  /  f ]_ (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) ) )  =  ( x  e.  ( ZZ>= `  M
)  |->  if ( x  <_  N ,  ( G `  ( J `
 x ) ) ,  ( G `  M ) ) ) )
117110, 116syl 14 . . . . . . . . . 10  |-  ( ph  ->  [_ J  /  f ]_ ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )  =  ( x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  ( J `  x )
) ,  ( G `
 M ) ) ) )
118108, 117syl5eq 2132 . . . . . . . . 9  |-  ( ph  ->  [_ J  /  f ]_ P  =  (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  ( J `  x )
) ,  ( G `
 M ) ) ) )
119118ad2antrr 472 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  [_ J  /  f ]_ P  =  ( x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( J `  x
) ) ,  ( G `  M ) ) ) )
120 2fveq3 5310 . . . . . . . . . 10  |-  ( x  =  b  ->  ( G `  ( J `  x ) )  =  ( G `  ( J `  b )
) )
12183, 120ifbieq1d 3413 . . . . . . . . 9  |-  ( x  =  b  ->  if ( x  <_  N , 
( G `  ( J `  x )
) ,  ( G `
 M ) )  =  if ( b  <_  N ,  ( G `  ( J `
 b ) ) ,  ( G `  M ) ) )
122121adantl 271 . . . . . . . 8  |-  ( ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  /\  x  =  b )  ->  if ( x  <_  N ,  ( G `  ( J `  x
) ) ,  ( G `  M ) )  =  if ( b  <_  N , 
( G `  ( J `  b )
) ,  ( G `
 M ) ) )
12337iftrued 3400 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( J `  b ) ) ,  ( G `
 M ) )  =  ( G `  ( J `  b ) ) )
124 fveq2 5305 . . . . . . . . . . 11  |-  ( a  =  ( J `  b )  ->  ( G `  a )  =  ( G `  ( J `  b ) ) )
125124eleq1d 2156 . . . . . . . . . 10  |-  ( a  =  ( J `  b )  ->  (
( G `  a
)  e.  S  <->  ( G `  ( J `  b
) )  e.  S
) )
126 elfzuz 9434 . . . . . . . . . . 11  |-  ( ( J `  b )  e.  ( M ... N )  ->  ( J `  b )  e.  ( ZZ>= `  M )
)
12755, 126syl 14 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  b )  e.  ( ZZ>= `  M )
)
128125, 98, 127rspcdva 2727 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( J `  b ) )  e.  S )
129123, 128eqeltrd 2164 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( J `  b ) ) ,  ( G `
 M ) )  e.  S )
130119, 122, 88, 129fvmptd 5385 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  if ( b  <_  N ,  ( G `  ( J `
 b ) ) ,  ( G `  M ) ) )
131130, 123eqtrd 2120 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  ( G `  ( J `  b ) ) )
13267, 107, 1313eqtr4rd 2131 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  ( [_ Q  /  f ]_ P `  b ) )
1331adantr 270 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  K  e.  ( M ... N ) )
13451adantr 270 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  J :
( M ... N
)
-1-1-onto-> ( M ... N ) )
13592adantlr 461 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( G `  x )  e.  S
)
136133, 134, 63, 135, 68iseqf1olemjpcl 9920 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( [_ J  /  f ]_ P `  x )  e.  S
)
137133, 134, 63, 135, 68iseqf1olemqpcl 9921 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( [_ Q  /  f ]_ P `  x )  e.  S
)
138 iseqf1o.1 . . . . . 6  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  e.  S )
139138adantlr 461 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  .+  y )  e.  S
)
14015, 132, 136, 137, 139seq3fveq 9891 . . . 4  |-  ( (
ph  /\  M  <  K )  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  ( K  -  1 ) )  =  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  ( K  -  1 ) ) )
141 iseqf1o.2 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  =  ( y 
.+  x ) )
142 iseqf1o.3 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S ) )  -> 
( ( x  .+  y )  .+  z
)  =  ( x 
.+  ( y  .+  z ) ) )
143 iseqf1o.4 . . . . . . 7  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
144 iseqf1o.6 . . . . . . 7  |-  ( ph  ->  F : ( M ... N ) -1-1-onto-> ( M ... N ) )
145 iseqf1olemstep.const . . . . . . 7  |-  ( ph  ->  A. x  e.  ( M..^ K ) ( J `  x )  =  x )
146 iseqf1olemnk . . . . . . 7  |-  ( ph  ->  K  =/=  ( `' J `  K ) )
147138, 141, 142, 143, 144, 92, 1, 51, 145, 146, 63, 68seq3f1olemqsumk 9924 . . . . . 6  |-  ( ph  ->  (  seq K ( 
.+  ,  [_ J  /  f ]_ P
) `  N )  =  (  seq K ( 
.+  ,  [_ Q  /  f ]_ P
) `  N )
)
148147adantr 270 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
1497zcnd 8867 . . . . . . . 8  |-  ( (
ph  /\  M  <  K )  ->  K  e.  CC )
150 npcan1 7854 . . . . . . . 8  |-  ( K  e.  CC  ->  (
( K  -  1 )  +  1 )  =  K )
151149, 150syl 14 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  ( ( K  -  1 )  +  1 )  =  K )
152151seqeq1d 9860 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  seq (
( K  -  1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P
)  =  seq K
(  .+  ,  [_ J  /  f ]_ P
) )
153152fveq1d 5307 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
) )
154151seqeq1d 9860 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  seq (
( K  -  1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P
)  =  seq K
(  .+  ,  [_ Q  /  f ]_ P
) )
155154fveq1d 5307 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
156148, 153, 1553eqtr4d 2130 . . . 4  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
157140, 156oveq12d 5670 . . 3  |-  ( (
ph  /\  M  <  K )  ->  ( (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  ( K  -  1 ) )  .+  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P ) `  N
) )  =  ( (  seq M ( 
.+  ,  [_ Q  /  f ]_ P
) `  ( K  -  1 ) ) 
.+  (  seq (
( K  -  1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P
) `  N )
) )
158142adantlr 461 . . . 4  |-  ( ( ( ph  /\  M  <  K )  /\  (
x  e.  S  /\  y  e.  S  /\  z  e.  S )
)  ->  ( (
x  .+  y )  .+  z )  =  ( x  .+  ( y 
.+  z ) ) )
159 elfzuz3 9435 . . . . . . 7  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
1601, 159syl 14 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= `  K ) )
161160adantr 270 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  N  e.  ( ZZ>= `  K )
)
162151fveq2d 5309 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  ( ZZ>= `  ( ( K  - 
1 )  +  1 ) )  =  (
ZZ>= `  K ) )
163161, 162eleqtrrd 2167 . . . 4  |-  ( (
ph  /\  M  <  K )  ->  N  e.  ( ZZ>= `  ( ( K  -  1 )  +  1 ) ) )
164139, 158, 163, 15, 136seq3split 9903 . . 3  |-  ( (
ph  /\  M  <  K )  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  ( (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  ( K  -  1 ) )  .+  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P ) `  N
) ) )
165139, 158, 163, 15, 137seq3split 9903 . . 3  |-  ( (
ph  /\  M  <  K )  ->  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  =  ( (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  ( K  -  1 ) )  .+  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P ) `  N
) ) )
166157, 164, 1653eqtr4d 2130 . 2  |-  ( (
ph  /\  M  <  K )  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
167147adantr 270 . . 3  |-  ( (
ph  /\  M  =  K )  ->  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
168 seqeq1 9857 . . . . . 6  |-  ( M  =  K  ->  seq M (  .+  ,  [_ J  /  f ]_ P )  =  seq K (  .+  ,  [_ J  /  f ]_ P ) )
169168fveq1d 5307 . . . . 5  |-  ( M  =  K  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
) )
170 seqeq1 9857 . . . . . 6  |-  ( M  =  K  ->  seq M (  .+  ,  [_ Q  /  f ]_ P )  =  seq K (  .+  ,  [_ Q  /  f ]_ P ) )
171170fveq1d 5307 . . . . 5  |-  ( M  =  K  ->  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
172169, 171eqeq12d 2102 . . . 4  |-  ( M  =  K  ->  (
(  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  <->  (  seq K
(  .+  ,  [_ J  /  f ]_ P
) `  N )  =  (  seq K ( 
.+  ,  [_ Q  /  f ]_ P
) `  N )
) )
173172adantl 271 . . 3  |-  ( (
ph  /\  M  =  K )  ->  (
(  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  <->  (  seq K
(  .+  ,  [_ J  /  f ]_ P
) `  N )  =  (  seq K ( 
.+  ,  [_ Q  /  f ]_ P
) `  N )
) )
174167, 173mpbird 165 . 2  |-  ( (
ph  /\  M  =  K )  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
175 elfzle1 9439 . . . 4  |-  ( K  e.  ( M ... N )  ->  M  <_  K )
1761, 175syl 14 . . 3  |-  ( ph  ->  M  <_  K )
177 zleloe 8795 . . . 4  |-  ( ( M  e.  ZZ  /\  K  e.  ZZ )  ->  ( M  <_  K  <->  ( M  <  K  \/  M  =  K )
) )
1783, 6, 177syl2anc 403 . . 3  |-  ( ph  ->  ( M  <_  K  <->  ( M  <  K  \/  M  =  K )
) )
179176, 178mpbid 145 . 2  |-  ( ph  ->  ( M  <  K  \/  M  =  K
) )
180166, 174, 179mpjaodan 747 1  |-  ( ph  ->  (  seq M ( 
.+  ,  [_ J  /  f ]_ P
) `  N )  =  (  seq M ( 
.+  ,  [_ Q  /  f ]_ P
) `  N )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 664    /\ w3a 924    = wceq 1289    e. wcel 1438    =/= wne 2255   A.wral 2359   _Vcvv 2619   [_csb 2933   ifcif 3393   class class class wbr 3845    |-> cmpt 3899   `'ccnv 4437   -->wf 5011   -1-1-onto->wf1o 5014   ` cfv 5015  (class class class)co 5652   Fincfn 6455   CCcc 7346   RRcr 7347   1c1 7349    + caddc 7351    < clt 7520    <_ cle 7521    - cmin 7651   ZZcz 8748   ZZ>=cuz 9017   ...cfz 9422  ..^cfzo 9549    seqcseq 9848
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3954  ax-sep 3957  ax-nul 3965  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-setind 4353  ax-iinf 4403  ax-cnex 7434  ax-resscn 7435  ax-1cn 7436  ax-1re 7437  ax-icn 7438  ax-addcl 7439  ax-addrcl 7440  ax-mulcl 7441  ax-addcom 7443  ax-addass 7445  ax-distr 7447  ax-i2m1 7448  ax-0lt1 7449  ax-0id 7451  ax-rnegex 7452  ax-cnre 7454  ax-pre-ltirr 7455  ax-pre-ltwlin 7456  ax-pre-lttrn 7457  ax-pre-apti 7458  ax-pre-ltadd 7459
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-if 3394  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-int 3689  df-iun 3732  df-br 3846  df-opab 3900  df-mpt 3901  df-tr 3937  df-id 4120  df-iord 4193  df-on 4195  df-ilim 4196  df-suc 4198  df-iom 4406  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022  df-fv 5023  df-riota 5608  df-ov 5655  df-oprab 5656  df-mpt2 5657  df-1st 5911  df-2nd 5912  df-recs 6070  df-frec 6156  df-1o 6181  df-er 6290  df-en 6456  df-fin 6458  df-pnf 7522  df-mnf 7523  df-xr 7524  df-ltxr 7525  df-le 7526  df-sub 7653  df-neg 7654  df-inn 8421  df-n0 8672  df-z 8749  df-uz 9018  df-fz 9423  df-fzo 9550  df-iseq 9849  df-seq3 9850
This theorem is referenced by:  seq3f1olemstep  9926
  Copyright terms: Public domain W3C validator