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

Theorem seq3f1olemqsum 10224
Description: Lemma for seq3f1o 10228. 
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 9756 . . . . . . . 8  |-  ( K  e.  ( M ... N )  ->  M  e.  ZZ )
31, 2syl 14 . . . . . . 7  |-  ( ph  ->  M  e.  ZZ )
43adantr 272 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  M  e.  ZZ )
5 elfzelz 9757 . . . . . . . . 9  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )
61, 5syl 14 . . . . . . . 8  |-  ( ph  ->  K  e.  ZZ )
76adantr 272 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  K  e.  ZZ )
8 peano2zm 9046 . . . . . . 7  |-  ( K  e.  ZZ  ->  ( K  -  1 )  e.  ZZ )
97, 8syl 14 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  ( K  -  1 )  e.  ZZ )
10 simpr 109 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  M  <  K )
11 zltlem1 9065 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  K  e.  ZZ )  ->  ( M  <  K  <->  M  <_  ( K  - 
1 ) ) )
124, 7, 11syl2anc 406 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  ( M  <  K  <->  M  <_  ( K  -  1 ) ) )
1310, 12mpbid 146 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  M  <_  ( K  -  1 ) )
14 eluz2 9284 . . . . . 6  |-  ( ( K  -  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( K  -  1 )  e.  ZZ  /\  M  <_ 
( K  -  1 ) ) )
154, 9, 13, 14syl3anbrc 1148 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  ( K  -  1 )  e.  ( ZZ>= `  M )
)
163ad2antrr 477 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  M  e.  ZZ )
17 elfzel2 9755 . . . . . . . . . . . 12  |-  ( K  e.  ( M ... N )  ->  N  e.  ZZ )
181, 17syl 14 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ZZ )
1918ad2antrr 477 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  N  e.  ZZ )
20 elfzelz 9757 . . . . . . . . . . 11  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  e.  ZZ )
2120adantl 273 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ZZ )
22 elfzle1 9758 . . . . . . . . . . 11  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  M  <_  b )
2322adantl 273 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  M  <_  b )
2421zred 9127 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  RR )
256ad2antrr 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  e.  ZZ )
2625zred 9127 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  e.  RR )
2719zred 9127 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  N  e.  RR )
28 peano2rem 7993 . . . . . . . . . . . . 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 9759 . . . . . . . . . . . . 13  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  <_  ( K  -  1 ) )
3130adantl 273 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  ( K  -  1 ) )
3226lem1d 8651 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( K  -  1 )  <_  K )
3324, 29, 26, 31, 32letrd 7850 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  K )
34 elfzle2 9759 . . . . . . . . . . . . 13  |-  ( K  e.  ( M ... N )  ->  K  <_  N )
351, 34syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  K  <_  N )
3635ad2antrr 477 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  <_  N )
3724, 26, 27, 33, 36letrd 7850 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  N )
38 elfz4 9750 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  b  e.  ZZ )  /\  ( M  <_  b  /\  b  <_  N ) )  ->  b  e.  ( M ... N ) )
3916, 19, 21, 23, 37, 38syl32anc 1207 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ( M ... N
) )
40 elfzel1 9756 . . . . . . . . . . . . . 14  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  e.  ZZ )
4140zred 9127 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  e.  RR )
42 elfzelz 9757 . . . . . . . . . . . . . 14  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  b  e.  ZZ )
4342zred 9127 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  b  e.  RR )
44 elfzle1 9758 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  <_  b )
4541, 43, 44lensymd 7848 . . . . . . . . . . . 12  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  -.  b  <  K )
46 zltlem1 9065 . . . . . . . . . . . . . 14  |-  ( ( b  e.  ZZ  /\  K  e.  ZZ )  ->  ( b  <  K  <->  b  <_  ( K  - 
1 ) ) )
4721, 25, 46syl2anc 406 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  (
b  <  K  <->  b  <_  ( K  -  1 ) ) )
4831, 47mpbird 166 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <  K )
4945, 48nsyl3 598 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  -.  b  e.  ( K ... ( `' J `  K ) ) )
5049iffalsed 3452 . . . . . . . . . 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 5333 . . . . . . . . . . . . 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 477 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  J : ( M ... N ) --> ( M ... N ) )
5554, 39ffvelrnd 5522 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  b )  e.  ( M ... N
) )
5650, 55eqeltrd 2192 . . . . . . . . 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 2176 . . . . . . . . . . 11  |-  ( u  =  b  ->  (
u  e.  ( K ... ( `' J `  K ) )  <->  b  e.  ( K ... ( `' J `  K ) ) ) )
58 eqeq1 2122 . . . . . . . . . . . 12  |-  ( u  =  b  ->  (
u  =  K  <->  b  =  K ) )
59 fvoveq1 5763 . . . . . . . . . . . 12  |-  ( u  =  b  ->  ( J `  ( u  -  1 ) )  =  ( J `  ( b  -  1 ) ) )
6058, 59ifbieq2d 3464 . . . . . . . . . . 11  |-  ( u  =  b  ->  if ( u  =  K ,  K ,  ( J `
 ( u  - 
1 ) ) )  =  if ( b  =  K ,  K ,  ( J `  ( b  -  1 ) ) ) )
61 fveq2 5387 . . . . . . . . . . 11  |-  ( u  =  b  ->  ( J `  u )  =  ( J `  b ) )
6257, 60, 61ifbieq12d 3466 . . . . . . . . . 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 5463 . . . . . . . . 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 406 . . . . . . . 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 2148 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( Q `  b )  =  ( J `  b ) )
6766fveq2d 5391 . . . . . 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 2997 . . . . . . . . . 10  |-  [_ Q  /  f ]_ P  =  [_ Q  /  f ]_ ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )
703, 18fzfigd 10155 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M ... N
)  e.  Fin )
71 mptexg 5611 . . . . . . . . . . . . 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, 72eqeltrid 2202 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  _V )
74 nfcvd 2257 . . . . . . . . . . . 12  |-  ( Q  e.  _V  ->  F/_ f
( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( Q `  x ) ) ,  ( G `
 M ) ) ) )
75 fveq1 5386 . . . . . . . . . . . . . . 15  |-  ( f  =  Q  ->  (
f `  x )  =  ( Q `  x ) )
7675fveq2d 5391 . . . . . . . . . . . . . 14  |-  ( f  =  Q  ->  ( G `  ( f `  x ) )  =  ( G `  ( Q `  x )
) )
7776ifeq1d 3457 . . . . . . . . . . . . 13  |-  ( f  =  Q  ->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) )  =  if ( x  <_  N ,  ( G `  ( Q `
 x ) ) ,  ( G `  M ) ) )
7877mpteq2dv 3987 . . . . . . . . . . . 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 3011 . . . . . . . . . . 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 2160 . . . . . . . . 9  |-  ( ph  ->  [_ Q  /  f ]_ P  =  (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  ( Q `  x )
) ,  ( G `
 M ) ) ) )
8281ad2antrr 477 . . . . . . . 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 3900 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  <_  N  <->  b  <_  N ) )
84 2fveq3 5392 . . . . . . . . . 10  |-  ( x  =  b  ->  ( G `  ( Q `  x ) )  =  ( G `  ( Q `  b )
) )
8583, 84ifbieq1d 3462 . . . . . . . . 9  |-  ( x  =  b  ->  if ( x  <_  N , 
( G `  ( Q `  x )
) ,  ( G `
 M ) )  =  if ( b  <_  N ,  ( G `  ( Q `
 b ) ) ,  ( G `  M ) ) )
8685adantl 273 . . . . . . . 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 9753 . . . . . . . . 9  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  e.  ( ZZ>= `  M )
)
8887adantl 273 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ( ZZ>= `  M )
)
8937iftrued 3449 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( Q `  b ) ) ,  ( G `
 M ) )  =  ( G `  ( Q `  b ) ) )
90 fveq2 5387 . . . . . . . . . . 11  |-  ( a  =  ( Q `  b )  ->  ( G `  a )  =  ( G `  ( Q `  b ) ) )
9190eleq1d 2184 . . . . . . . . . 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 2480 . . . . . . . . . . . 12  |-  ( ph  ->  A. x  e.  (
ZZ>= `  M ) ( G `  x )  e.  S )
94 fveq2 5387 . . . . . . . . . . . . . 14  |-  ( x  =  a  ->  ( G `  x )  =  ( G `  a ) )
9594eleq1d 2184 . . . . . . . . . . . . 13  |-  ( x  =  a  ->  (
( G `  x
)  e.  S  <->  ( G `  a )  e.  S
) )
9695cbvralv 2629 . . . . . . . . . . . 12  |-  ( A. x  e.  ( ZZ>= `  M ) ( G `
 x )  e.  S  <->  A. a  e.  (
ZZ>= `  M ) ( G `  a )  e.  S )
9793, 96sylib 121 . . . . . . . . . . 11  |-  ( ph  ->  A. a  e.  (
ZZ>= `  M ) ( G `  a )  e.  S )
9897ad2antrr 477 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  A. a  e.  ( ZZ>= `  M )
( G `  a
)  e.  S )
991, 51, 63iseqf1olemqf 10215 . . . . . . . . . . . . 13  |-  ( ph  ->  Q : ( M ... N ) --> ( M ... N ) )
10099ad2antrr 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  Q : ( M ... N ) --> ( M ... N ) )
101100, 39ffvelrnd 5522 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( Q `  b )  e.  ( M ... N
) )
102 elfzuz 9753 . . . . . . . . . . 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 2766 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( Q `  b ) )  e.  S )
10589, 104eqeltrd 2192 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( Q `  b ) ) ,  ( G `
 M ) )  e.  S )
10682, 86, 88, 105fvmptd 5468 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ Q  /  f ]_ P `  b )  =  if ( b  <_  N ,  ( G `  ( Q `
 b ) ) ,  ( G `  M ) ) )
107106, 89eqtrd 2148 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ Q  /  f ]_ P `  b )  =  ( G `  ( Q `  b ) ) )
10868csbeq2i 2997 . . . . . . . . . 10  |-  [_ J  /  f ]_ P  =  [_ J  /  f ]_ ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )
109 fex 5613 . . . . . . . . . . . 12  |-  ( ( J : ( M ... N ) --> ( M ... N )  /\  ( M ... N )  e.  Fin )  ->  J  e.  _V )
11053, 70, 109syl2anc 406 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  _V )
111 nfcvd 2257 . . . . . . . . . . . 12  |-  ( J  e.  _V  ->  F/_ f
( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( J `  x ) ) ,  ( G `
 M ) ) ) )
112 fveq1 5386 . . . . . . . . . . . . . . 15  |-  ( f  =  J  ->  (
f `  x )  =  ( J `  x ) )
113112fveq2d 5391 . . . . . . . . . . . . . 14  |-  ( f  =  J  ->  ( G `  ( f `  x ) )  =  ( G `  ( J `  x )
) )
114113ifeq1d 3457 . . . . . . . . . . . . 13  |-  ( f  =  J  ->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) )  =  if ( x  <_  N ,  ( G `  ( J `
 x ) ) ,  ( G `  M ) ) )
115114mpteq2dv 3987 . . . . . . . . . . . 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 3011 . . . . . . . . . . 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 2160 . . . . . . . . 9  |-  ( ph  ->  [_ J  /  f ]_ P  =  (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  ( J `  x )
) ,  ( G `
 M ) ) ) )
119118ad2antrr 477 . . . . . . . 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 5392 . . . . . . . . . 10  |-  ( x  =  b  ->  ( G `  ( J `  x ) )  =  ( G `  ( J `  b )
) )
12183, 120ifbieq1d 3462 . . . . . . . . 9  |-  ( x  =  b  ->  if ( x  <_  N , 
( G `  ( J `  x )
) ,  ( G `
 M ) )  =  if ( b  <_  N ,  ( G `  ( J `
 b ) ) ,  ( G `  M ) ) )
122121adantl 273 . . . . . . . 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 3449 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( J `  b ) ) ,  ( G `
 M ) )  =  ( G `  ( J `  b ) ) )
124 fveq2 5387 . . . . . . . . . . 11  |-  ( a  =  ( J `  b )  ->  ( G `  a )  =  ( G `  ( J `  b ) ) )
125124eleq1d 2184 . . . . . . . . . 10  |-  ( a  =  ( J `  b )  ->  (
( G `  a
)  e.  S  <->  ( G `  ( J `  b
) )  e.  S
) )
126 elfzuz 9753 . . . . . . . . . . 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 2766 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( J `  b ) )  e.  S )
129123, 128eqeltrd 2192 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( J `  b ) ) ,  ( G `
 M ) )  e.  S )
130119, 122, 88, 129fvmptd 5468 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  if ( b  <_  N ,  ( G `  ( J `
 b ) ) ,  ( G `  M ) ) )
131130, 123eqtrd 2148 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  ( G `  ( J `  b ) ) )
13267, 107, 1313eqtr4rd 2159 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  ( [_ Q  /  f ]_ P `  b ) )
1331adantr 272 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  K  e.  ( M ... N ) )
13451adantr 272 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  J :
( M ... N
)
-1-1-onto-> ( M ... N ) )
13592adantlr 466 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( G `  x )  e.  S
)
136133, 134, 63, 135, 68iseqf1olemjpcl 10219 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( [_ J  /  f ]_ P `  x )  e.  S
)
137133, 134, 63, 135, 68iseqf1olemqpcl 10220 . . . . 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 466 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  .+  y )  e.  S
)
14015, 132, 136, 137, 139seq3fveq 10195 . . . 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 10223 . . . . . 6  |-  ( ph  ->  (  seq K ( 
.+  ,  [_ J  /  f ]_ P
) `  N )  =  (  seq K ( 
.+  ,  [_ Q  /  f ]_ P
) `  N )
)
148147adantr 272 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
1497zcnd 9128 . . . . . . . 8  |-  ( (
ph  /\  M  <  K )  ->  K  e.  CC )
150 npcan1 8104 . . . . . . . 8  |-  ( K  e.  CC  ->  (
( K  -  1 )  +  1 )  =  K )
151149, 150syl 14 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  ( ( K  -  1 )  +  1 )  =  K )
152151seqeq1d 10175 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  seq (
( K  -  1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P
)  =  seq K
(  .+  ,  [_ J  /  f ]_ P
) )
153152fveq1d 5389 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
) )
154151seqeq1d 10175 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  seq (
( K  -  1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P
)  =  seq K
(  .+  ,  [_ Q  /  f ]_ P
) )
155154fveq1d 5389 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
156148, 153, 1553eqtr4d 2158 . . . 4  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
157140, 156oveq12d 5758 . . 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 466 . . . 4  |-  ( ( ( ph  /\  M  <  K )  /\  (
x  e.  S  /\  y  e.  S  /\  z  e.  S )
)  ->  ( (
x  .+  y )  .+  z )  =  ( x  .+  ( y 
.+  z ) ) )
159 elfzuz3 9754 . . . . . . 7  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
1601, 159syl 14 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= `  K ) )
161160adantr 272 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  N  e.  ( ZZ>= `  K )
)
162151fveq2d 5391 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  ( ZZ>= `  ( ( K  - 
1 )  +  1 ) )  =  (
ZZ>= `  K ) )
163161, 162eleqtrrd 2195 . . . 4  |-  ( (
ph  /\  M  <  K )  ->  N  e.  ( ZZ>= `  ( ( K  -  1 )  +  1 ) ) )
164139, 158, 163, 15, 136seq3split 10203 . . 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 10203 . . 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 2158 . 2  |-  ( (
ph  /\  M  <  K )  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
167147adantr 272 . . 3  |-  ( (
ph  /\  M  =  K )  ->  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
168 seqeq1 10172 . . . . . 6  |-  ( M  =  K  ->  seq M (  .+  ,  [_ J  /  f ]_ P )  =  seq K (  .+  ,  [_ J  /  f ]_ P ) )
169168fveq1d 5389 . . . . 5  |-  ( M  =  K  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
) )
170 seqeq1 10172 . . . . . 6  |-  ( M  =  K  ->  seq M (  .+  ,  [_ Q  /  f ]_ P )  =  seq K (  .+  ,  [_ Q  /  f ]_ P ) )
171170fveq1d 5389 . . . . 5  |-  ( M  =  K  ->  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
172169, 171eqeq12d 2130 . . . 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 273 . . 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 166 . 2  |-  ( (
ph  /\  M  =  K )  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
175 elfzle1 9758 . . . 4  |-  ( K  e.  ( M ... N )  ->  M  <_  K )
1761, 175syl 14 . . 3  |-  ( ph  ->  M  <_  K )
177 zleloe 9055 . . . 4  |-  ( ( M  e.  ZZ  /\  K  e.  ZZ )  ->  ( M  <_  K  <->  ( M  <  K  \/  M  =  K )
) )
1783, 6, 177syl2anc 406 . . 3  |-  ( ph  ->  ( M  <_  K  <->  ( M  <  K  \/  M  =  K )
) )
179176, 178mpbid 146 . 2  |-  ( ph  ->  ( M  <  K  \/  M  =  K
) )
180166, 174, 179mpjaodan 770 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 103    <-> wb 104    \/ wo 680    /\ w3a 945    = wceq 1314    e. wcel 1463    =/= wne 2283   A.wral 2391   _Vcvv 2658   [_csb 2973   ifcif 3442   class class class wbr 3897    |-> cmpt 3957   `'ccnv 4506   -->wf 5087   -1-1-onto->wf1o 5090   ` cfv 5091  (class class class)co 5740   Fincfn 6600   CCcc 7582   RRcr 7583   1c1 7585    + caddc 7587    < clt 7764    <_ cle 7765    - cmin 7897   ZZcz 9008   ZZ>=cuz 9278   ...cfz 9741  ..^cfzo 9870    seqcseq 10169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-addcom 7684  ax-addass 7686  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-0id 7692  ax-rnegex 7693  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-frec 6254  df-1o 6279  df-er 6395  df-en 6601  df-fin 6603  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-inn 8681  df-n0 8932  df-z 9009  df-uz 9279  df-fz 9742  df-fzo 9871  df-seqfrec 10170
This theorem is referenced by:  seq3f1olemstep  10225
  Copyright terms: Public domain W3C validator