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

Theorem seq3f1olemqsum 10449
Description: Lemma for seq3f1o 10453. 
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 9973 . . . . . . . 8  |-  ( K  e.  ( M ... N )  ->  M  e.  ZZ )
31, 2syl 14 . . . . . . 7  |-  ( ph  ->  M  e.  ZZ )
43adantr 274 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  M  e.  ZZ )
5 elfzelz 9974 . . . . . . . . 9  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )
61, 5syl 14 . . . . . . . 8  |-  ( ph  ->  K  e.  ZZ )
76adantr 274 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  K  e.  ZZ )
8 peano2zm 9243 . . . . . . 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 9262 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  K  e.  ZZ )  ->  ( M  <  K  <->  M  <_  ( K  - 
1 ) ) )
124, 7, 11syl2anc 409 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  ( M  <  K  <->  M  <_  ( K  -  1 ) ) )
1310, 12mpbid 146 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  M  <_  ( K  -  1 ) )
14 eluz2 9486 . . . . . 6  |-  ( ( K  -  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( K  -  1 )  e.  ZZ  /\  M  <_ 
( K  -  1 ) ) )
154, 9, 13, 14syl3anbrc 1176 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  ( K  -  1 )  e.  ( ZZ>= `  M )
)
163ad2antrr 485 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  M  e.  ZZ )
17 elfzel2 9972 . . . . . . . . . . . 12  |-  ( K  e.  ( M ... N )  ->  N  e.  ZZ )
181, 17syl 14 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ZZ )
1918ad2antrr 485 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  N  e.  ZZ )
20 elfzelz 9974 . . . . . . . . . . 11  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  e.  ZZ )
2120adantl 275 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ZZ )
22 elfzle1 9976 . . . . . . . . . . 11  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  M  <_  b )
2322adantl 275 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  M  <_  b )
2421zred 9327 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  RR )
256ad2antrr 485 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  e.  ZZ )
2625zred 9327 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  e.  RR )
2719zred 9327 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  N  e.  RR )
28 peano2rem 8179 . . . . . . . . . . . . 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 9977 . . . . . . . . . . . . 13  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  <_  ( K  -  1 ) )
3130adantl 275 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  ( K  -  1 ) )
3226lem1d 8842 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( K  -  1 )  <_  K )
3324, 29, 26, 31, 32letrd 8036 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  K )
34 elfzle2 9977 . . . . . . . . . . . . 13  |-  ( K  e.  ( M ... N )  ->  K  <_  N )
351, 34syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  K  <_  N )
3635ad2antrr 485 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  K  <_  N )
3724, 26, 27, 33, 36letrd 8036 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  <_  N )
38 elfz4 9967 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  b  e.  ZZ )  /\  ( M  <_  b  /\  b  <_  N ) )  ->  b  e.  ( M ... N ) )
3916, 19, 21, 23, 37, 38syl32anc 1241 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ( M ... N
) )
40 elfzel1 9973 . . . . . . . . . . . . . 14  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  e.  ZZ )
4140zred 9327 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  e.  RR )
42 elfzelz 9974 . . . . . . . . . . . . . 14  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  b  e.  ZZ )
4342zred 9327 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  b  e.  RR )
44 elfzle1 9976 . . . . . . . . . . . . 13  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  K  <_  b )
4541, 43, 44lensymd 8034 . . . . . . . . . . . 12  |-  ( b  e.  ( K ... ( `' J `  K ) )  ->  -.  b  <  K )
46 zltlem1 9262 . . . . . . . . . . . . . 14  |-  ( ( b  e.  ZZ  /\  K  e.  ZZ )  ->  ( b  <  K  <->  b  <_  ( K  - 
1 ) ) )
4721, 25, 46syl2anc 409 . . . . . . . . . . . . 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 621 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  -.  b  e.  ( K ... ( `' J `  K ) ) )
5049iffalsed 3535 . . . . . . . . . 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 5440 . . . . . . . . . . . . 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 485 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  J : ( M ... N ) --> ( M ... N ) )
5554, 39ffvelrnd 5630 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( J `  b )  e.  ( M ... N
) )
5650, 55eqeltrd 2247 . . . . . . . . 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 2231 . . . . . . . . . . 11  |-  ( u  =  b  ->  (
u  e.  ( K ... ( `' J `  K ) )  <->  b  e.  ( K ... ( `' J `  K ) ) ) )
58 eqeq1 2177 . . . . . . . . . . . 12  |-  ( u  =  b  ->  (
u  =  K  <->  b  =  K ) )
59 fvoveq1 5874 . . . . . . . . . . . 12  |-  ( u  =  b  ->  ( J `  ( u  -  1 ) )  =  ( J `  ( b  -  1 ) ) )
6058, 59ifbieq2d 3549 . . . . . . . . . . 11  |-  ( u  =  b  ->  if ( u  =  K ,  K ,  ( J `
 ( u  - 
1 ) ) )  =  if ( b  =  K ,  K ,  ( J `  ( b  -  1 ) ) ) )
61 fveq2 5494 . . . . . . . . . . 11  |-  ( u  =  b  ->  ( J `  u )  =  ( J `  b ) )
6257, 60, 61ifbieq12d 3551 . . . . . . . . . 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 5570 . . . . . . . . 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 409 . . . . . . . 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 2203 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( Q `  b )  =  ( J `  b ) )
6766fveq2d 5498 . . . . . 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 3076 . . . . . . . . . 10  |-  [_ Q  /  f ]_ P  =  [_ Q  /  f ]_ ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )
703, 18fzfigd 10380 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M ... N
)  e.  Fin )
71 mptexg 5719 . . . . . . . . . . . . 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 2257 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  _V )
74 nfcvd 2313 . . . . . . . . . . . 12  |-  ( Q  e.  _V  ->  F/_ f
( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( Q `  x ) ) ,  ( G `
 M ) ) ) )
75 fveq1 5493 . . . . . . . . . . . . . . 15  |-  ( f  =  Q  ->  (
f `  x )  =  ( Q `  x ) )
7675fveq2d 5498 . . . . . . . . . . . . . 14  |-  ( f  =  Q  ->  ( G `  ( f `  x ) )  =  ( G `  ( Q `  x )
) )
7776ifeq1d 3542 . . . . . . . . . . . . 13  |-  ( f  =  Q  ->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) )  =  if ( x  <_  N ,  ( G `  ( Q `
 x ) ) ,  ( G `  M ) ) )
7877mpteq2dv 4078 . . . . . . . . . . . 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 3092 . . . . . . . . . . 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, 80eqtrid 2215 . . . . . . . . 9  |-  ( ph  ->  [_ Q  /  f ]_ P  =  (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  ( Q `  x )
) ,  ( G `
 M ) ) ) )
8281ad2antrr 485 . . . . . . . 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 3990 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  <_  N  <->  b  <_  N ) )
84 2fveq3 5499 . . . . . . . . . 10  |-  ( x  =  b  ->  ( G `  ( Q `  x ) )  =  ( G `  ( Q `  b )
) )
8583, 84ifbieq1d 3547 . . . . . . . . 9  |-  ( x  =  b  ->  if ( x  <_  N , 
( G `  ( Q `  x )
) ,  ( G `
 M ) )  =  if ( b  <_  N ,  ( G `  ( Q `
 b ) ) ,  ( G `  M ) ) )
8685adantl 275 . . . . . . . 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 9970 . . . . . . . . 9  |-  ( b  e.  ( M ... ( K  -  1
) )  ->  b  e.  ( ZZ>= `  M )
)
8887adantl 275 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  b  e.  ( ZZ>= `  M )
)
8937iftrued 3532 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( Q `  b ) ) ,  ( G `
 M ) )  =  ( G `  ( Q `  b ) ) )
90 fveq2 5494 . . . . . . . . . . 11  |-  ( a  =  ( Q `  b )  ->  ( G `  a )  =  ( G `  ( Q `  b ) ) )
9190eleq1d 2239 . . . . . . . . . 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 2543 . . . . . . . . . . . 12  |-  ( ph  ->  A. x  e.  (
ZZ>= `  M ) ( G `  x )  e.  S )
94 fveq2 5494 . . . . . . . . . . . . . 14  |-  ( x  =  a  ->  ( G `  x )  =  ( G `  a ) )
9594eleq1d 2239 . . . . . . . . . . . . 13  |-  ( x  =  a  ->  (
( G `  x
)  e.  S  <->  ( G `  a )  e.  S
) )
9695cbvralv 2696 . . . . . . . . . . . 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 485 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  A. a  e.  ( ZZ>= `  M )
( G `  a
)  e.  S )
991, 51, 63iseqf1olemqf 10440 . . . . . . . . . . . . 13  |-  ( ph  ->  Q : ( M ... N ) --> ( M ... N ) )
10099ad2antrr 485 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  Q : ( M ... N ) --> ( M ... N ) )
101100, 39ffvelrnd 5630 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( Q `  b )  e.  ( M ... N
) )
102 elfzuz 9970 . . . . . . . . . . 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 2839 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( Q `  b ) )  e.  S )
10589, 104eqeltrd 2247 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( Q `  b ) ) ,  ( G `
 M ) )  e.  S )
10682, 86, 88, 105fvmptd 5575 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ Q  /  f ]_ P `  b )  =  if ( b  <_  N ,  ( G `  ( Q `
 b ) ) ,  ( G `  M ) ) )
107106, 89eqtrd 2203 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ Q  /  f ]_ P `  b )  =  ( G `  ( Q `  b ) ) )
10868csbeq2i 3076 . . . . . . . . . 10  |-  [_ J  /  f ]_ P  =  [_ J  /  f ]_ ( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x
) ) ,  ( G `  M ) ) )
109 fex 5723 . . . . . . . . . . . 12  |-  ( ( J : ( M ... N ) --> ( M ... N )  /\  ( M ... N )  e.  Fin )  ->  J  e.  _V )
11053, 70, 109syl2anc 409 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  _V )
111 nfcvd 2313 . . . . . . . . . . . 12  |-  ( J  e.  _V  ->  F/_ f
( x  e.  (
ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( J `  x ) ) ,  ( G `
 M ) ) ) )
112 fveq1 5493 . . . . . . . . . . . . . . 15  |-  ( f  =  J  ->  (
f `  x )  =  ( J `  x ) )
113112fveq2d 5498 . . . . . . . . . . . . . 14  |-  ( f  =  J  ->  ( G `  ( f `  x ) )  =  ( G `  ( J `  x )
) )
114113ifeq1d 3542 . . . . . . . . . . . . 13  |-  ( f  =  J  ->  if ( x  <_  N , 
( G `  (
f `  x )
) ,  ( G `
 M ) )  =  if ( x  <_  N ,  ( G `  ( J `
 x ) ) ,  ( G `  M ) ) )
115114mpteq2dv 4078 . . . . . . . . . . . 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 3092 . . . . . . . . . . 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, 117eqtrid 2215 . . . . . . . . 9  |-  ( ph  ->  [_ J  /  f ]_ P  =  (
x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N , 
( G `  ( J `  x )
) ,  ( G `
 M ) ) ) )
119118ad2antrr 485 . . . . . . . 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 5499 . . . . . . . . . 10  |-  ( x  =  b  ->  ( G `  ( J `  x ) )  =  ( G `  ( J `  b )
) )
12183, 120ifbieq1d 3547 . . . . . . . . 9  |-  ( x  =  b  ->  if ( x  <_  N , 
( G `  ( J `  x )
) ,  ( G `
 M ) )  =  if ( b  <_  N ,  ( G `  ( J `
 b ) ) ,  ( G `  M ) ) )
122121adantl 275 . . . . . . . 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 3532 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( J `  b ) ) ,  ( G `
 M ) )  =  ( G `  ( J `  b ) ) )
124 fveq2 5494 . . . . . . . . . . 11  |-  ( a  =  ( J `  b )  ->  ( G `  a )  =  ( G `  ( J `  b ) ) )
125124eleq1d 2239 . . . . . . . . . 10  |-  ( a  =  ( J `  b )  ->  (
( G `  a
)  e.  S  <->  ( G `  ( J `  b
) )  e.  S
) )
126 elfzuz 9970 . . . . . . . . . . 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 2839 . . . . . . . . 9  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( G `  ( J `  b ) )  e.  S )
129123, 128eqeltrd 2247 . . . . . . . 8  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  if ( b  <_  N ,  ( G `  ( J `  b ) ) ,  ( G `
 M ) )  e.  S )
130119, 122, 88, 129fvmptd 5575 . . . . . . 7  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  if ( b  <_  N ,  ( G `  ( J `
 b ) ) ,  ( G `  M ) ) )
131130, 123eqtrd 2203 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  ( G `  ( J `  b ) ) )
13267, 107, 1313eqtr4rd 2214 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  b  e.  ( M ... ( K  -  1 ) ) )  ->  ( [_ J  /  f ]_ P `  b )  =  ( [_ Q  /  f ]_ P `  b ) )
1331adantr 274 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  K  e.  ( M ... N ) )
13451adantr 274 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  J :
( M ... N
)
-1-1-onto-> ( M ... N ) )
13592adantlr 474 . . . . . 6  |-  ( ( ( ph  /\  M  <  K )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( G `  x )  e.  S
)
136133, 134, 63, 135, 68iseqf1olemjpcl 10444 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( [_ J  /  f ]_ P `  x )  e.  S
)
137133, 134, 63, 135, 68iseqf1olemqpcl 10445 . . . . 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 474 . . . . 5  |-  ( ( ( ph  /\  M  <  K )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  .+  y )  e.  S
)
14015, 132, 136, 137, 139seq3fveq 10420 . . . 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 10448 . . . . . 6  |-  ( ph  ->  (  seq K ( 
.+  ,  [_ J  /  f ]_ P
) `  N )  =  (  seq K ( 
.+  ,  [_ Q  /  f ]_ P
) `  N )
)
148147adantr 274 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
1497zcnd 9328 . . . . . . . 8  |-  ( (
ph  /\  M  <  K )  ->  K  e.  CC )
150 npcan1 8290 . . . . . . . 8  |-  ( K  e.  CC  ->  (
( K  -  1 )  +  1 )  =  K )
151149, 150syl 14 . . . . . . 7  |-  ( (
ph  /\  M  <  K )  ->  ( ( K  -  1 )  +  1 )  =  K )
152151seqeq1d 10400 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  seq (
( K  -  1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P
)  =  seq K
(  .+  ,  [_ J  /  f ]_ P
) )
153152fveq1d 5496 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
) )
154151seqeq1d 10400 . . . . . 6  |-  ( (
ph  /\  M  <  K )  ->  seq (
( K  -  1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P
)  =  seq K
(  .+  ,  [_ Q  /  f ]_ P
) )
155154fveq1d 5496 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
156148, 153, 1553eqtr4d 2213 . . . 4  |-  ( (
ph  /\  M  <  K )  ->  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq ( ( K  - 
1 )  +  1 ) (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
157140, 156oveq12d 5869 . . 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 474 . . . 4  |-  ( ( ( ph  /\  M  <  K )  /\  (
x  e.  S  /\  y  e.  S  /\  z  e.  S )
)  ->  ( (
x  .+  y )  .+  z )  =  ( x  .+  ( y 
.+  z ) ) )
159 elfzuz3 9971 . . . . . . 7  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
1601, 159syl 14 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= `  K ) )
161160adantr 274 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  N  e.  ( ZZ>= `  K )
)
162151fveq2d 5498 . . . . 5  |-  ( (
ph  /\  M  <  K )  ->  ( ZZ>= `  ( ( K  - 
1 )  +  1 ) )  =  (
ZZ>= `  K ) )
163161, 162eleqtrrd 2250 . . . 4  |-  ( (
ph  /\  M  <  K )  ->  N  e.  ( ZZ>= `  ( ( K  -  1 )  +  1 ) ) )
164139, 158, 163, 15, 136seq3split 10428 . . 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 10428 . . 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 2213 . 2  |-  ( (
ph  /\  M  <  K )  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
167147adantr 274 . . 3  |-  ( (
ph  /\  M  =  K )  ->  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
168 seqeq1 10397 . . . . . 6  |-  ( M  =  K  ->  seq M (  .+  ,  [_ J  /  f ]_ P )  =  seq K (  .+  ,  [_ J  /  f ]_ P ) )
169168fveq1d 5496 . . . . 5  |-  ( M  =  K  ->  (  seq M (  .+  ,  [_ J  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ J  /  f ]_ P ) `  N
) )
170 seqeq1 10397 . . . . . 6  |-  ( M  =  K  ->  seq M (  .+  ,  [_ Q  /  f ]_ P )  =  seq K (  .+  ,  [_ Q  /  f ]_ P ) )
171170fveq1d 5496 . . . . 5  |-  ( M  =  K  ->  (  seq M (  .+  ,  [_ Q  /  f ]_ P ) `  N
)  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  N
) )
172169, 171eqeq12d 2185 . . . 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 275 . . 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 9976 . . . 4  |-  ( K  e.  ( M ... N )  ->  M  <_  K )
1761, 175syl 14 . . 3  |-  ( ph  ->  M  <_  K )
177 zleloe 9252 . . . 4  |-  ( ( M  e.  ZZ  /\  K  e.  ZZ )  ->  ( M  <_  K  <->  ( M  <  K  \/  M  =  K )
) )
1783, 6, 177syl2anc 409 . . 3  |-  ( ph  ->  ( M  <_  K  <->  ( M  <  K  \/  M  =  K )
) )
179176, 178mpbid 146 . 2  |-  ( ph  ->  ( M  <  K  \/  M  =  K
) )
180166, 174, 179mpjaodan 793 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 703    /\ w3a 973    = wceq 1348    e. wcel 2141    =/= wne 2340   A.wral 2448   _Vcvv 2730   [_csb 3049   ifcif 3525   class class class wbr 3987    |-> cmpt 4048   `'ccnv 4608   -->wf 5192   -1-1-onto->wf1o 5195   ` cfv 5196  (class class class)co 5851   Fincfn 6716   CCcc 7765   RRcr 7766   1c1 7768    + caddc 7770    < clt 7947    <_ cle 7948    - cmin 8083   ZZcz 9205   ZZ>=cuz 9480   ...cfz 9958  ..^cfzo 10091    seqcseq 10394
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7858  ax-resscn 7859  ax-1cn 7860  ax-1re 7861  ax-icn 7862  ax-addcl 7863  ax-addrcl 7864  ax-mulcl 7865  ax-addcom 7867  ax-addass 7869  ax-distr 7871  ax-i2m1 7872  ax-0lt1 7873  ax-0id 7875  ax-rnegex 7876  ax-cnre 7878  ax-pre-ltirr 7879  ax-pre-ltwlin 7880  ax-pre-lttrn 7881  ax-pre-apti 7882  ax-pre-ltadd 7883
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-riota 5807  df-ov 5854  df-oprab 5855  df-mpo 5856  df-1st 6117  df-2nd 6118  df-recs 6282  df-frec 6368  df-1o 6393  df-er 6511  df-en 6717  df-fin 6719  df-pnf 7949  df-mnf 7950  df-xr 7951  df-ltxr 7952  df-le 7953  df-sub 8085  df-neg 8086  df-inn 8872  df-n0 9129  df-z 9206  df-uz 9481  df-fz 9959  df-fzo 10092  df-seqfrec 10395
This theorem is referenced by:  seq3f1olemstep  10450
  Copyright terms: Public domain W3C validator