Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem24 Structured version   Visualization version   Unicode version

Theorem poimirlem24 32028
Description: Lemma for poimir 32037, two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimirlem28.1  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  C )
poimirlem28.2  |-  ( (
ph  /\  p :
( 1 ... N
) --> ( 0 ... K ) )  ->  B  e.  ( 0 ... N ) )
poimirlem25.3  |-  ( ph  ->  T : ( 1 ... N ) --> ( 0..^ K ) )
poimirlem25.4  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem24.5  |-  ( ph  ->  V  e.  ( 0 ... N ) )
Assertion
Ref Expression
poimirlem24  |-  ( ph  ->  ( E. x  e.  ( ( ( 0 ... K )  ^m  ( 1 ... N
) )  ^m  (
0 ... ( N  - 
1 ) ) ) ( x  =  ( y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  /\  ( ( 0 ... ( N  - 
1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  E. p  e.  ran  x
( p `  N
)  =/=  0 ) )  <->  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  { V } ) i  = 
[_ <. T ,  U >.  /  s ]_ C  /\  -.  ( V  =  N  /\  ( ( T `  N )  =  0  /\  ( U `  N )  =  N ) ) ) ) )
Distinct variable groups:    i, j, p, s, x, y, ph    j, N, y    T, j, y    U, j, y    j, V, y    ph, i, p, s    B, i, j, s   
i, K, j, p, s    i, N, p, s    T, i, p    U, i, p    T, s    ph, x    x, B, y    C, i, p, x, y    x, K, y    x, N    x, T    U, s, x    i, V, p, s, x
Allowed substitution hints:    B( p)    C( j, s)

Proof of Theorem poimirlem24
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 nfv 1769 . . . . . . . . 9  |-  F/ j ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )
2 nfcsb1v 3365 . . . . . . . . . 10  |-  F/_ j [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )
3 nfcv 2612 . . . . . . . . . 10  |-  F/_ j
( 1 ... N
)
4 nfcv 2612 . . . . . . . . . 10  |-  F/_ j
( 0 ... K
)
52, 3, 4nff 5735 . . . . . . . . 9  |-  F/ j
[_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K )
61, 5nfim 2023 . . . . . . . 8  |-  F/ j ( ( ph  /\  y  e.  ( 0 ... ( N  - 
1 ) ) )  ->  [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )
7 eleq1 2537 . . . . . . . . . 10  |-  ( j  =  y  ->  (
j  e.  ( 0 ... ( N  - 
1 ) )  <->  y  e.  ( 0 ... ( N  -  1 ) ) ) )
87anbi2d 718 . . . . . . . . 9  |-  ( j  =  y  ->  (
( ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  <->  ( ph  /\  y  e.  ( 0 ... ( N  - 
1 ) ) ) ) )
9 csbeq1a 3358 . . . . . . . . . 10  |-  ( j  =  y  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  [_ y  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) )
109feq1d 5724 . . . . . . . . 9  |-  ( j  =  y  ->  (
( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K )  <->  [_ y  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) ) )
118, 10imbi12d 327 . . . . . . . 8  |-  ( j  =  y  ->  (
( ( ph  /\  j  e.  ( 0 ... ( N  - 
1 ) ) )  ->  ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )  <->  ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  [_ y  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) ) ) )
12 poimir.0 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN )
1312nncnd 10647 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
14 npcan1 10065 . . . . . . . . . . . . 13  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
1513, 14syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
1612nnzd 11062 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  ZZ )
17 peano2zm 11004 . . . . . . . . . . . . . 14  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
1816, 17syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
19 uzid 11197 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
20 peano2uz 11235 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
2118, 19, 203syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
2215, 21eqeltrrd 2550 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
23 fzss2 11864 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... N
) )
2422, 23syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
2524sselda 3418 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  j  e.  ( 0 ... N
) )
26 elun 3565 . . . . . . . . . . . . 13  |-  ( y  e.  ( { 1 }  u.  { 0 } )  <->  ( y  e.  { 1 }  \/  y  e.  { 0 } ) )
27 fzofzp1 12037 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 0..^ K )  ->  ( x  +  1 )  e.  ( 0 ... K
) )
28 elsni 3985 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { 1 }  ->  y  =  1 )
2928oveq2d 6324 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { 1 }  ->  ( x  +  y )  =  ( x  +  1 ) )
3029eleq1d 2533 . . . . . . . . . . . . . . 15  |-  ( y  e.  { 1 }  ->  ( ( x  +  y )  e.  ( 0 ... K
)  <->  ( x  + 
1 )  e.  ( 0 ... K ) ) )
3127, 30syl5ibrcom 230 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 0..^ K )  ->  ( y  e.  { 1 }  ->  ( x  +  y )  e.  ( 0 ... K ) ) )
32 elfzoelz 11947 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 0..^ K )  ->  x  e.  ZZ )
3332zcnd 11064 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 0..^ K )  ->  x  e.  CC )
3433addid1d 9851 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 0..^ K )  ->  ( x  +  0 )  =  x )
35 elfzofz 11962 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 0..^ K )  ->  x  e.  ( 0 ... K
) )
3634, 35eqeltrd 2549 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 0..^ K )  ->  ( x  +  0 )  e.  ( 0 ... K
) )
37 elsni 3985 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { 0 }  ->  y  =  0 )
3837oveq2d 6324 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { 0 }  ->  ( x  +  y )  =  ( x  +  0 ) )
3938eleq1d 2533 . . . . . . . . . . . . . . 15  |-  ( y  e.  { 0 }  ->  ( ( x  +  y )  e.  ( 0 ... K
)  <->  ( x  + 
0 )  e.  ( 0 ... K ) ) )
4036, 39syl5ibrcom 230 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 0..^ K )  ->  ( y  e.  { 0 }  ->  ( x  +  y )  e.  ( 0 ... K ) ) )
4131, 40jaod 387 . . . . . . . . . . . . 13  |-  ( x  e.  ( 0..^ K )  ->  ( (
y  e.  { 1 }  \/  y  e. 
{ 0 } )  ->  ( x  +  y )  e.  ( 0 ... K ) ) )
4226, 41syl5bi 225 . . . . . . . . . . . 12  |-  ( x  e.  ( 0..^ K )  ->  ( y  e.  ( { 1 }  u.  { 0 } )  ->  ( x  +  y )  e.  ( 0 ... K
) ) )
4342imp 436 . . . . . . . . . . 11  |-  ( ( x  e.  ( 0..^ K )  /\  y  e.  ( { 1 }  u.  { 0 } ) )  ->  (
x  +  y )  e.  ( 0 ... K ) )
4443adantl 473 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  ( 0..^ K )  /\  y  e.  ( { 1 }  u.  { 0 } ) ) )  -> 
( x  +  y )  e.  ( 0 ... K ) )
45 poimirlem25.3 . . . . . . . . . . 11  |-  ( ph  ->  T : ( 1 ... N ) --> ( 0..^ K ) )
4645adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  T : ( 1 ... N ) --> ( 0..^ K ) )
47 1ex 9656 . . . . . . . . . . . . . 14  |-  1  e.  _V
4847fconst 5782 . . . . . . . . . . . . 13  |-  ( ( U " ( 1 ... j ) )  X.  { 1 } ) : ( U
" ( 1 ... j ) ) --> { 1 }
49 c0ex 9655 . . . . . . . . . . . . . 14  |-  0  e.  _V
5049fconst 5782 . . . . . . . . . . . . 13  |-  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( U
" ( ( j  +  1 ) ... N ) ) --> { 0 }
5148, 50pm3.2i 462 . . . . . . . . . . . 12  |-  ( ( ( U " (
1 ... j ) )  X.  { 1 } ) : ( U
" ( 1 ... j ) ) --> { 1 }  /\  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } ) : ( U " ( ( j  +  1 ) ... N ) ) --> { 0 } )
52 poimirlem25.4 . . . . . . . . . . . . . 14  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
53 dff1o3 5834 . . . . . . . . . . . . . . 15  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( U :
( 1 ... N
) -onto-> ( 1 ... N )  /\  Fun  `' U ) )
5453simprbi 471 . . . . . . . . . . . . . 14  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' U
)
55 imain 5669 . . . . . . . . . . . . . 14  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... j
) )  i^i  ( U " ( ( j  +  1 ) ... N ) ) ) )
5652, 54, 553syl 18 . . . . . . . . . . . . 13  |-  ( ph  ->  ( U " (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) ) )  =  ( ( U " ( 1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) ) )
57 elfznn0 11913 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... N )  ->  j  e.  NN0 )
5857nn0red 10950 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
5958ltp1d 10559 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... N )  ->  j  <  ( j  +  1 ) )
60 fzdisj 11852 . . . . . . . . . . . . . . . 16  |-  ( j  <  ( j  +  1 )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
6159, 60syl 17 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... N )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
6261imaeq2d 5174 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  ( U " (/) ) )
63 ima0 5189 . . . . . . . . . . . . . 14  |-  ( U
" (/) )  =  (/)
6462, 63syl6eq 2521 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  (/) )
6556, 64sylan9req 2526 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( U " (
1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) )  =  (/) )
66 fun 5758 . . . . . . . . . . . 12  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } ) : ( U "
( 1 ... j
) ) --> { 1 }  /\  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( U
" ( ( j  +  1 ) ... N ) ) --> { 0 } )  /\  ( ( U "
( 1 ... j
) )  i^i  ( U " ( ( j  +  1 ) ... N ) ) )  =  (/) )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) : ( ( U
" ( 1 ... j ) )  u.  ( U " (
( j  +  1 ) ... N ) ) ) --> ( { 1 }  u.  {
0 } ) )
6751, 65, 66sylancr 676 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) : ( ( U
" ( 1 ... j ) )  u.  ( U " (
( j  +  1 ) ... N ) ) ) --> ( { 1 }  u.  {
0 } ) )
68 nn0p1nn 10933 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  NN )
6957, 68syl 17 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  NN )
70 nnuz 11218 . . . . . . . . . . . . . . . . 17  |-  NN  =  ( ZZ>= `  1 )
7169, 70syl6eleq 2559 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
72 elfzuz3 11823 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  j )
)
73 fzsplit2 11850 . . . . . . . . . . . . . . . 16  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  j )
)  ->  ( 1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
7471, 72, 73syl2anc 673 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... N )  ->  (
1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
7574imaeq2d 5174 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( 1 ... N ) )  =  ( U " (
( 1 ... j
)  u.  ( ( j  +  1 ) ... N ) ) ) )
76 imaundi 5254 . . . . . . . . . . . . . 14  |-  ( U
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... j
) )  u.  ( U " ( ( j  +  1 ) ... N ) ) )
7775, 76syl6req 2522 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... N )  ->  (
( U " (
1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... N
) ) )  =  ( U " (
1 ... N ) ) )
78 f1ofo 5835 . . . . . . . . . . . . . 14  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U :
( 1 ... N
) -onto-> ( 1 ... N ) )
79 foima 5811 . . . . . . . . . . . . . 14  |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N )  -> 
( U " (
1 ... N ) )  =  ( 1 ... N ) )
8052, 78, 793syl 18 . . . . . . . . . . . . 13  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( 1 ... N ) )
8177, 80sylan9eqr 2527 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( U " (
1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... N
) ) )  =  ( 1 ... N
) )
8281feq2d 5725 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) : ( ( U " ( 1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... N
) ) ) --> ( { 1 }  u.  { 0 } )  <->  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  { 0 } ) ) )
8367, 82mpbid 215 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  {
0 } ) )
84 ovex 6336 . . . . . . . . . . 11  |-  ( 1 ... N )  e. 
_V
8584a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
1 ... N )  e. 
_V )
86 inidm 3632 . . . . . . . . . 10  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
8744, 46, 83, 85, 85, 86off 6565 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
8825, 87syldan 478 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
896, 11, 88chvar 2119 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  [_ y  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
90 fzp1elp1 11875 . . . . . . . . 9  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  ( 0 ... ( ( N  - 
1 )  +  1 ) ) )
9115oveq2d 6324 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... (
( N  -  1 )  +  1 ) )  =  ( 0 ... N ) )
9291eleq2d 2534 . . . . . . . . . 10  |-  ( ph  ->  ( ( y  +  1 )  e.  ( 0 ... ( ( N  -  1 )  +  1 ) )  <-> 
( y  +  1 )  e.  ( 0 ... N ) ) )
9392biimpa 492 . . . . . . . . 9  |-  ( (
ph  /\  ( y  +  1 )  e.  ( 0 ... (
( N  -  1 )  +  1 ) ) )  ->  (
y  +  1 )  e.  ( 0 ... N ) )
9490, 93sylan2 482 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  +  1 )  e.  ( 0 ... N ) )
95 nfv 1769 . . . . . . . . . 10  |-  F/ j ( ph  /\  (
y  +  1 )  e.  ( 0 ... N ) )
96 nfcsb1v 3365 . . . . . . . . . . 11  |-  F/_ j [_ ( y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )
9796, 3, 4nff 5735 . . . . . . . . . 10  |-  F/ j
[_ ( y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K )
9895, 97nfim 2023 . . . . . . . . 9  |-  F/ j ( ( ph  /\  ( y  +  1 )  e.  ( 0 ... N ) )  ->  [_ ( y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )
99 ovex 6336 . . . . . . . . 9  |-  ( y  +  1 )  e. 
_V
100 eleq1 2537 . . . . . . . . . . 11  |-  ( j  =  ( y  +  1 )  ->  (
j  e.  ( 0 ... N )  <->  ( y  +  1 )  e.  ( 0 ... N
) ) )
101100anbi2d 718 . . . . . . . . . 10  |-  ( j  =  ( y  +  1 )  ->  (
( ph  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  ( y  +  1 )  e.  ( 0 ... N ) ) ) )
102 csbeq1a 3358 . . . . . . . . . . 11  |-  ( j  =  ( y  +  1 )  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  [_ (
y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) )
103102feq1d 5724 . . . . . . . . . 10  |-  ( j  =  ( y  +  1 )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K )  <->  [_ ( y  +  1 )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) ) )
104101, 103imbi12d 327 . . . . . . . . 9  |-  ( j  =  ( y  +  1 )  ->  (
( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )  <->  ( ( ph  /\  ( y  +  1 )  e.  ( 0 ... N ) )  ->  [_ ( y  +  1 )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) ) ) )
10598, 99, 104, 87vtoclf 3085 . . . . . . . 8  |-  ( (
ph  /\  ( y  +  1 )  e.  ( 0 ... N
) )  ->  [_ (
y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
10694, 105syldan 478 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  [_ (
y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
107 csbeq1 3352 . . . . . . . . 9  |-  ( y  =  if ( y  <  V ,  y ,  ( y  +  1 ) )  ->  [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  = 
[_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
108107feq1d 5724 . . . . . . . 8  |-  ( y  =  if ( y  <  V ,  y ,  ( y  +  1 ) )  -> 
( [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K )  <->  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
109 csbeq1 3352 . . . . . . . . 9  |-  ( ( y  +  1 )  =  if ( y  <  V ,  y ,  ( y  +  1 ) )  ->  [_ ( y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  = 
[_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
110109feq1d 5724 . . . . . . . 8  |-  ( ( y  +  1 )  =  if ( y  <  V ,  y ,  ( y  +  1 ) )  -> 
( [_ ( y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K )  <->  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
111108, 110ifboth 3908 . . . . . . 7  |-  ( (
[_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K )  /\  [_ (
y  +  1 )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )  ->  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
11289, 106, 111syl2anc 673 . . . . . 6  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )
113 ovex 6336 . . . . . . 7  |-  ( 0 ... K )  e. 
_V
114113, 84elmap 7518 . . . . . 6  |-  ( [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  e.  ( ( 0 ... K )  ^m  (
1 ... N ) )  <->  [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )
115112, 114sylibr 217 . . . . 5  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  e.  ( ( 0 ... K )  ^m  (
1 ... N ) ) )
116 eqid 2471 . . . . 5  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
117115, 116fmptd 6061 . . . 4  |-  ( ph  ->  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) : ( 0 ... ( N  -  1 ) ) --> ( ( 0 ... K )  ^m  ( 1 ... N ) ) )
118 ovex 6336 . . . . 5  |-  ( ( 0 ... K )  ^m  ( 1 ... N ) )  e. 
_V
119 ovex 6336 . . . . 5  |-  ( 0 ... ( N  - 
1 ) )  e. 
_V
120118, 119elmap 7518 . . . 4  |-  ( ( y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  e.  ( ( ( 0 ... K )  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) )  <->  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) : ( 0 ... ( N  -  1 ) ) --> ( ( 0 ... K )  ^m  ( 1 ... N ) ) )
121117, 120sylibr 217 . . 3  |-  ( ph  ->  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  e.  ( ( ( 0 ... K )  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )
122 rneq 5066 . . . . . . . 8  |-  ( x  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  ->  ran  x  =  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) )
123122mpteq1d 4477 . . . . . . 7  |-  ( x  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  ->  ( p  e. 
ran  x  |->  B )  =  ( p  e. 
ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B ) )
124123rneqd 5068 . . . . . 6  |-  ( x  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  ->  ran  ( p  e.  ran  x  |->  B )  =  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B ) )
125124sseq2d 3446 . . . . 5  |-  ( x  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  ->  ( ( 0 ... ( N  - 
1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  <->  ( 0 ... ( N  - 
1 ) )  C_  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B ) ) )
126122rexeqdv 2980 . . . . 5  |-  ( x  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  ->  ( E. p  e.  ran  x ( p `
 N )  =/=  0  <->  E. p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) ( p `  N
)  =/=  0 ) )
127125, 126anbi12d 725 . . . 4  |-  ( x  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  ->  ( ( ( 0 ... ( N  -  1 ) ) 
C_  ran  ( p  e.  ran  x  |->  B )  /\  E. p  e. 
ran  x ( p `
 N )  =/=  0 )  <->  ( (
0 ... ( N  - 
1 ) )  C_  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )  /\  E. p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) ( p `  N
)  =/=  0 ) ) )
128127ceqsrexv 3160 . . 3  |-  ( ( y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  e.  ( ( ( 0 ... K )  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) )  ->  ( E. x  e.  (
( ( 0 ... K )  ^m  (
1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) ( x  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  /\  ( ( 0 ... ( N  - 
1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  E. p  e.  ran  x
( p `  N
)  =/=  0 ) )  <->  ( ( 0 ... ( N  - 
1 ) )  C_  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )  /\  E. p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) ( p `  N
)  =/=  0 ) ) )
129121, 128syl 17 . 2  |-  ( ph  ->  ( E. x  e.  ( ( ( 0 ... K )  ^m  ( 1 ... N
) )  ^m  (
0 ... ( N  - 
1 ) ) ) ( x  =  ( y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )  /\  ( ( 0 ... ( N  - 
1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  E. p  e.  ran  x
( p `  N
)  =/=  0 ) )  <->  ( ( 0 ... ( N  - 
1 ) )  C_  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )  /\  E. p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) ( p `  N
)  =/=  0 ) ) )
130 dfss3 3408 . . . 4  |-  ( ( 0 ... ( N  -  1 ) ) 
C_  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )  <->  A. i  e.  ( 0 ... ( N  -  1 ) ) i  e.  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B ) )
131 ovex 6336 . . . . . . . . . . . . 13  |-  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  e. 
_V
132 poimirlem28.1 . . . . . . . . . . . . 13  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  C )
133131, 132csbie 3375 . . . . . . . . . . . 12  |-  [_ (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  /  p ]_ B  =  C
134133csbeq2i 3786 . . . . . . . . . . 11  |-  [_ <. T ,  U >.  /  s ]_ [_ ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B  =  [_ <. T ,  U >.  /  s ]_ C
135 opex 4664 . . . . . . . . . . . . 13  |-  <. T ,  U >.  e.  _V
136135a1i 11 . . . . . . . . . . . 12  |-  ( ph  -> 
<. T ,  U >.  e. 
_V )
137 fveq2 5879 . . . . . . . . . . . . . . 15  |-  ( s  =  <. T ,  U >.  ->  ( 1st `  s
)  =  ( 1st `  <. T ,  U >. ) )
138 fex 6155 . . . . . . . . . . . . . . . . 17  |-  ( ( T : ( 1 ... N ) --> ( 0..^ K )  /\  ( 1 ... N
)  e.  _V )  ->  T  e.  _V )
13945, 84, 138sylancl 675 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  _V )
140 f1oexrnex 6761 . . . . . . . . . . . . . . . . 17  |-  ( ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  /\  ( 1 ... N
)  e.  _V )  ->  U  e.  _V )
14152, 84, 140sylancl 675 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  U  e.  _V )
142 op1stg 6824 . . . . . . . . . . . . . . . 16  |-  ( ( T  e.  _V  /\  U  e.  _V )  ->  ( 1st `  <. T ,  U >. )  =  T )
143139, 141, 142syl2anc 673 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  <. T ,  U >. )  =  T )
144137, 143sylan9eqr 2527 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  =  <. T ,  U >. )  ->  ( 1st `  s
)  =  T )
145 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( s  =  <. T ,  U >.  ->  ( 2nd `  s
)  =  ( 2nd `  <. T ,  U >. ) )
146 op2ndg 6825 . . . . . . . . . . . . . . . . 17  |-  ( ( T  e.  _V  /\  U  e.  _V )  ->  ( 2nd `  <. T ,  U >. )  =  U )
147139, 141, 146syl2anc 673 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 2nd `  <. T ,  U >. )  =  U )
148145, 147sylan9eqr 2527 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  =  <. T ,  U >. )  ->  ( 2nd `  s
)  =  U )
149 imaeq1 5169 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  s )  =  U  ->  (
( 2nd `  s
) " ( 1 ... j ) )  =  ( U "
( 1 ... j
) ) )
150149xpeq1d 4862 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  s )  =  U  ->  (
( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  =  ( ( U " ( 1 ... j ) )  X.  { 1 } ) )
151 imaeq1 5169 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  s )  =  U  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  =  ( U "
( ( j  +  1 ) ... N
) ) )
152151xpeq1d 4862 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  s )  =  U  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) )
153150, 152uneq12d 3580 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  s )  =  U  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) )  =  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )
154148, 153syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  =  <. T ,  U >. )  ->  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) )  =  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )
155144, 154oveq12d 6326 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  =  <. T ,  U >. )  ->  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  =  ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
156155csbeq1d 3356 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  =  <. T ,  U >. )  ->  [_ ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B  =  [_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B )
157136, 156csbied 3376 . . . . . . . . . . 11  |-  ( ph  ->  [_ <. T ,  U >.  /  s ]_ [_ (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  /  p ]_ B  =  [_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  /  p ]_ B )
158134, 157syl5eqr 2519 . . . . . . . . . 10  |-  ( ph  ->  [_ <. T ,  U >.  /  s ]_ C  =  [_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B )
159158csbeq2dv 3785 . . . . . . . . 9  |-  ( ph  ->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  /  p ]_ B )
160159eqeq2d 2481 . . . . . . . 8  |-  ( ph  ->  ( i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  <->  i  =  [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B ) )
161160rexbidv 2892 . . . . . . 7  |-  ( ph  ->  ( E. y  e.  ( 0 ... ( N  -  1 ) ) i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  <->  E. y  e.  ( 0 ... ( N  -  1 ) ) i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B ) )
162 vex 3034 . . . . . . . . 9  |-  i  e. 
_V
163 eqid 2471 . . . . . . . . . 10  |-  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )  =  ( p  e.  ran  (
y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )
164163elrnmpt 5087 . . . . . . . . 9  |-  ( i  e.  _V  ->  (
i  e.  ran  (
p  e.  ran  (
y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )  <->  E. p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) i  =  B ) )
165162, 164ax-mp 5 . . . . . . . 8  |-  ( i  e.  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )  <->  E. p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) i  =  B )
166 nfv 1769 . . . . . . . . 9  |-  F/ k  i  =  B
167 nfcsb1v 3365 . . . . . . . . . 10  |-  F/_ p [_ k  /  p ]_ B
168167nfeq2 2627 . . . . . . . . 9  |-  F/ p  i  =  [_ k  /  p ]_ B
169 csbeq1a 3358 . . . . . . . . . 10  |-  ( p  =  k  ->  B  =  [_ k  /  p ]_ B )
170169eqeq2d 2481 . . . . . . . . 9  |-  ( p  =  k  ->  (
i  =  B  <->  i  =  [_ k  /  p ]_ B ) )
171166, 168, 170cbvrex 3002 . . . . . . . 8  |-  ( E. p  e.  ran  (
y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) i  =  B  <->  E. k  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) i  =  [_ k  /  p ]_ B )
172 ovex 6336 . . . . . . . . . . 11  |-  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
173172csbex 4531 . . . . . . . . . 10  |-  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  e. 
_V
174173rgenw 2768 . . . . . . . . 9  |-  A. y  e.  ( 0 ... ( N  -  1 ) ) [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
175 csbeq1 3352 . . . . . . . . . . . 12  |-  ( k  =  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  ->  [_ k  /  p ]_ B  =  [_ [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B )
176 vex 3034 . . . . . . . . . . . . . 14  |-  y  e. 
_V
177176, 99ifex 3940 . . . . . . . . . . . . 13  |-  if ( y  <  V , 
y ,  ( y  +  1 ) )  e.  _V
178 csbnestg 3791 . . . . . . . . . . . . 13  |-  ( if ( y  <  V ,  y ,  ( y  +  1 ) )  e.  _V  ->  [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B  =  [_ [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B )
179177, 178ax-mp 5 . . . . . . . . . . . 12  |-  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B  =  [_ [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B
180175, 179syl6eqr 2523 . . . . . . . . . . 11  |-  ( k  =  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  ->  [_ k  /  p ]_ B  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B )
181180eqeq2d 2481 . . . . . . . . . 10  |-  ( k  =  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  ->  ( i  =  [_ k  /  p ]_ B  <->  i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B ) )
182116, 181rexrnmpt 6047 . . . . . . . . 9  |-  ( A. y  e.  ( 0 ... ( N  - 
1 ) ) [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  e. 
_V  ->  ( E. k  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) i  =  [_ k  /  p ]_ B  <->  E. y  e.  ( 0 ... ( N  -  1 ) ) i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B ) )
183174, 182ax-mp 5 . . . . . . . 8  |-  ( E. k  e.  ran  (
y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) i  =  [_ k  /  p ]_ B  <->  E. y  e.  ( 0 ... ( N  -  1 ) ) i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B )
184165, 171, 1833bitri 279 . . . . . . 7  |-  ( i  e.  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B )  <->  E. y  e.  ( 0 ... ( N  -  1 ) ) i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  /  p ]_ B )
185161, 184syl6bbr 271 . . . . . 6  |-  ( ph  ->  ( E. y  e.  ( 0 ... ( N  -  1 ) ) i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  <->  i  e.  ran  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) 
|->  B ) ) )
18624sselda 3418 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  e.  ( 0 ... N
) )
187186adantr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  V )  ->  y  e.  ( 0 ... N
) )
188 elfzelz 11826 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  ZZ )
189188zred 11063 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  RR )
190189adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  e.  RR )
191 ltne 9748 . . . . . . . . . . . . 13  |-  ( ( y  e.  RR  /\  y  <  V )  ->  V  =/=  y )
192191necomd 2698 . . . . . . . . . . . 12  |-  ( ( y  e.  RR  /\  y  <  V )  -> 
y  =/=  V )
193190, 192sylan 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  V )  ->  y  =/=  V )
194 eldifsn 4088 . . . . . . . . . . 11  |-  ( y  e.  ( ( 0 ... N )  \  { V } )  <->  ( y  e.  ( 0 ... N
)  /\  y  =/=  V ) )
195187, 193, 194sylanbrc 677 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  V )  ->  y  e.  ( ( 0 ... N )  \  { V } ) )
19694adantr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  -.  y  <  V )  -> 
( y  +  1 )  e.  ( 0 ... N ) )
197 poimirlem24.5 . . . . . . . . . . . . . . 15  |-  ( ph  ->  V  e.  ( 0 ... N ) )
198 elfzelz 11826 . . . . . . . . . . . . . . 15  |-  ( V  e.  ( 0 ... N )  ->  V  e.  ZZ )
199197, 198syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  V  e.  ZZ )
200199zred 11063 . . . . . . . . . . . . 13  |-  ( ph  ->  V  e.  RR )
201200ad2antrr 740 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  -.  y  <  V )  ->  V  e.  RR )
202 zre 10965 . . . . . . . . . . . . . . . 16  |-  ( V  e.  ZZ  ->  V  e.  RR )
203 zre 10965 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ZZ  ->  y  e.  RR )
204 lenlt 9730 . . . . . . . . . . . . . . . 16  |-  ( ( V  e.  RR  /\  y  e.  RR )  ->  ( V  <_  y  <->  -.  y  <  V ) )
205202, 203, 204syl2an 485 . . . . . . . . . . . . . . 15  |-  ( ( V  e.  ZZ  /\  y  e.  ZZ )  ->  ( V  <_  y  <->  -.  y  <  V ) )
206 zleltp1 11011 . . . . . . . . . . . . . . 15  |-  ( ( V  e.  ZZ  /\  y  e.  ZZ )  ->  ( V  <_  y  <->  V  <  ( y  +  1 ) ) )
207205, 206bitr3d 263 . . . . . . . . . . . . . 14  |-  ( ( V  e.  ZZ  /\  y  e.  ZZ )  ->  ( -.  y  < 
V  <->  V  <  ( y  +  1 ) ) )
208199, 188, 207syl2an 485 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( -.  y  <  V  <->  V  <  ( y  +  1 ) ) )
209208biimpa 492 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  -.  y  <  V )  ->  V  <  ( y  +  1 ) )
210201, 209gtned 9787 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  -.  y  <  V )  -> 
( y  +  1 )  =/=  V )
211 eldifsn 4088 . . . . . . . . . . 11  |-  ( ( y  +  1 )  e.  ( ( 0 ... N )  \  { V } )  <->  ( (
y  +  1 )  e.  ( 0 ... N )  /\  (
y  +  1 )  =/=  V ) )
212196, 210, 211sylanbrc 677 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  -.  y  <  V )  -> 
( y  +  1 )  e.  ( ( 0 ... N ) 
\  { V }
) )
213195, 212ifclda 3904 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  e.  ( ( 0 ... N ) 
\  { V }
) )
214 nfcsb1v 3365 . . . . . . . . . . . 12  |-  F/_ j [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
215214nfeq2 2627 . . . . . . . . . . 11  |-  F/ j  i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_
<. T ,  U >.  /  s ]_ C
216 csbeq1a 3358 . . . . . . . . . . . 12  |-  ( j  =  if ( y  <  V ,  y ,  ( y  +  1 ) )  ->  [_ <. T ,  U >.  /  s ]_ C  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C )
217216eqeq2d 2481 . . . . . . . . . . 11  |-  ( j  =  if ( y  <  V ,  y ,  ( y  +  1 ) )  -> 
( i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
) )
218215, 217rspce 3131 . . . . . . . . . 10  |-  ( ( if ( y  < 
V ,  y ,  ( y  +  1 ) )  e.  ( ( 0 ... N
)  \  { V } )  /\  i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C )  ->  E. j  e.  ( ( 0 ... N )  \  { V } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
)
219218ex 441 . . . . . . . . 9  |-  ( if ( y  <  V ,  y ,  ( y  +  1 ) )  e.  ( ( 0 ... N ) 
\  { V }
)  ->  ( i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  E. j  e.  ( ( 0 ... N
)  \  { V } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
) )
220213, 219syl 17 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  ->  E. j  e.  (
( 0 ... N
)  \  { V } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
) )
221220rexlimdva 2871 . . . . . . 7  |-  ( ph  ->  ( E. y  e.  ( 0 ... ( N  -  1 ) ) i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  ->  E. j  e.  (
( 0 ... N
)  \  { V } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
) )
222 nfv 1769 . . . . . . . 8  |-  F/ j
ph
223 nfcv 2612 . . . . . . . . 9  |-  F/_ j
( 0 ... ( N  -  1 ) )
224223, 215nfrex 2848 . . . . . . . 8  |-  F/ j E. y  e.  ( 0 ... ( N  -  1 ) ) i  =  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ [_
<. T ,  U >.  /  s ]_ C
225 eldifi 3544 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  -> 
j  e.  ( 0 ... N ) )
226225, 57syl 17 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  -> 
j  e.  NN0 )
227226nn0ge0d 10952 . . . . . . . . . . . . 13  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  -> 
0  <_  j )
228227ad2antlr 741 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
0  <_  j )
229226nn0red 10950 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  -> 
j  e.  RR )
230229ad2antlr 741 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
j  e.  RR )
231200ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  ->  V  e.  RR )
23216zred 11063 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  RR )
233232ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  ->  N  e.  RR )
234 simpr 468 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
j  <  V )
235 elfzle2 11829 . . . . . . . . . . . . . . . 16  |-  ( V  e.  ( 0 ... N )  ->  V  <_  N )
236197, 235syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  V  <_  N )
237236ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  ->  V  <_  N )
238230, 231, 233, 234, 237ltletrd 9812 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
j  <  N )
239226nn0zd 11061 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  -> 
j  e.  ZZ )
240 zltlem1 11013 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ZZ  /\  N  e.  ZZ )  ->  ( j  <  N  <->  j  <_  ( N  - 
1 ) ) )
241239, 16, 240syl2anr 486 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  -> 
( j  <  N  <->  j  <_  ( N  - 
1 ) ) )
242241adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
( j  <  N  <->  j  <_  ( N  - 
1 ) ) )
243238, 242mpbid 215 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
j  <_  ( N  -  1 ) )
244 0z 10972 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
245 elfz 11816 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ZZ  /\  0  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  -> 
( j  e.  ( 0 ... ( N  -  1 ) )  <-> 
( 0  <_  j  /\  j  <_  ( N  -  1 ) ) ) )
246244, 245mp3an2 1378 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ZZ  /\  ( N  -  1
)  e.  ZZ )  ->  ( j  e.  ( 0 ... ( N  -  1 ) )  <->  ( 0  <_ 
j  /\  j  <_  ( N  -  1 ) ) ) )
247239, 18, 246syl2anr 486 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  -> 
( j  e.  ( 0 ... ( N  -  1 ) )  <-> 
( 0  <_  j  /\  j  <_  ( N  -  1 ) ) ) )
248247adantr 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
( j  e.  ( 0 ... ( N  -  1 ) )  <-> 
( 0  <_  j  /\  j  <_  ( N  -  1 ) ) ) )
249228, 243, 248mpbir2and 936 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
j  e.  ( 0 ... ( N  - 
1 ) ) )
250 0red 9662 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  0  e.  RR )
251200ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  V  e.  RR )
252229ad2antlr 741 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  j  e.  RR )
253 elfzle1 11828 . . . . . . . . . . . . . . . . 17  |-  ( V  e.  ( 0 ... N )  ->  0  <_  V )
254197, 253syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <_  V )
255254ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  0  <_  V
)
256 lenlt 9730 . . . . . . . . . . . . . . . . . 18  |-  ( ( V  e.  RR  /\  j  e.  RR )  ->  ( V  <_  j  <->  -.  j  <  V ) )
257200, 229, 256syl2an 485 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  -> 
( V  <_  j  <->  -.  j  <  V ) )
258257biimpar 493 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  V  <_  j
)
259 eldifsni 4089 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  -> 
j  =/=  V )
260259ad2antlr 741 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  j  =/=  V
)
261 ltlen 9753 . . . . . . . . . . . . . . . . . 18  |-  ( ( V  e.  RR  /\  j  e.  RR )  ->  ( V  <  j  <->  ( V  <_  j  /\  j  =/=  V ) ) )
262200, 229, 261syl2an 485 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  -> 
( V  <  j  <->  ( V  <_  j  /\  j  =/=  V ) ) )
263262adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  ( V  < 
j  <->  ( V  <_ 
j  /\  j  =/=  V ) ) )
264258, 260, 263mpbir2and 936 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  V  <  j
)
265250, 251, 252, 255, 264lelttrd 9810 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  0  <  j
)
266 zgt0ge1 11014 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ZZ  ->  (
0  <  j  <->  1  <_  j ) )
267239, 266syl 17 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  -> 
( 0  <  j  <->  1  <_  j ) )
268267ad2antlr 741 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  ( 0  < 
j  <->  1  <_  j
) )
269265, 268mpbid 215 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  1  <_  j
)
270 elfzle2 11829 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... N )  ->  j  <_  N )
271225, 270syl 17 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  -> 
j  <_  N )
272271ad2antlr 741 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  j  <_  N
)
273 1z 10991 . . . . . . . . . . . . . . . 16  |-  1  e.  ZZ
274 elfz 11816 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ZZ  /\  1  e.  ZZ  /\  N  e.  ZZ )  ->  (
j  e.  ( 1 ... N )  <->  ( 1  <_  j  /\  j  <_  N ) ) )
275273, 274mp3an2 1378 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ZZ  /\  N  e.  ZZ )  ->  ( j  e.  ( 1 ... N )  <-> 
( 1  <_  j  /\  j  <_  N ) ) )
276239, 16, 275syl2anr 486 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  -> 
( j  e.  ( 1 ... N )  <-> 
( 1  <_  j  /\  j  <_  N ) ) )
277276adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  ( j  e.  ( 1 ... N
)  <->  ( 1  <_ 
j  /\  j  <_  N ) ) )
278269, 272, 277mpbir2and 936 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  j  e.  ( 1 ... N ) )
279 elfzmlbm 11926 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... N )  ->  (
j  -  1 )  e.  ( 0 ... ( N  -  1 ) ) )
280278, 279syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  -.  j  <  V )  ->  ( j  - 
1 )  e.  ( 0 ... ( N  -  1 ) ) )
281249, 280ifclda 3904 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  ->  if ( j  <  V ,  j ,  ( j  -  1 ) )  e.  ( 0 ... ( N  - 
1 ) ) )
282 breq1 4398 . . . . . . . . . . . . . . . 16  |-  ( j  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  -> 
( j  <  V  <->  if ( j  <  V ,  j ,  ( j  -  1 ) )  <  V ) )
283 id 22 . . . . . . . . . . . . . . . 16  |-  ( j  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  -> 
j  =  if ( j  <  V , 
j ,  ( j  -  1 ) ) )
284 oveq1 6315 . . . . . . . . . . . . . . . 16  |-  ( j  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  -> 
( j  +  1 )  =  ( if ( j  <  V ,  j ,  ( j  -  1 ) )  +  1 ) )
285282, 283, 284ifbieq12d 3899 . . . . . . . . . . . . . . 15  |-  ( j  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  ->  if ( j  <  V ,  j ,  ( j  +  1 ) )  =  if ( if ( j  < 
V ,  j ,  ( j  -  1 ) )  <  V ,  if ( j  < 
V ,  j ,  ( j  -  1 ) ) ,  ( if ( j  < 
V ,  j ,  ( j  -  1 ) )  +  1 ) ) )
286285eqeq2d 2481 . . . . . . . . . . . . . 14  |-  ( j  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  -> 
( j  =  if ( j  <  V ,  j ,  ( j  +  1 ) )  <->  j  =  if ( if ( j  <  V ,  j ,  ( j  - 
1 ) )  < 
V ,  if ( j  <  V , 
j ,  ( j  -  1 ) ) ,  ( if ( j  <  V , 
j ,  ( j  -  1 ) )  +  1 ) ) ) )
287 breq1 4398 . . . . . . . . . . . . . . . 16  |-  ( ( j  -  1 )  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  -> 
( ( j  - 
1 )  <  V  <->  if ( j  <  V ,  j ,  ( j  -  1 ) )  <  V ) )
288 id 22 . . . . . . . . . . . . . . . 16  |-  ( ( j  -  1 )  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  -> 
( j  -  1 )  =  if ( j  <  V , 
j ,  ( j  -  1 ) ) )
289 oveq1 6315 . . . . . . . . . . . . . . . 16  |-  ( ( j  -  1 )  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  -> 
( ( j  - 
1 )  +  1 )  =  ( if ( j  <  V ,  j ,  ( j  -  1 ) )  +  1 ) )
290287, 288, 289ifbieq12d 3899 . . . . . . . . . . . . . . 15  |-  ( ( j  -  1 )  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  ->  if ( ( j  - 
1 )  <  V ,  ( j  - 
1 ) ,  ( ( j  -  1 )  +  1 ) )  =  if ( if ( j  < 
V ,  j ,  ( j  -  1 ) )  <  V ,  if ( j  < 
V ,  j ,  ( j  -  1 ) ) ,  ( if ( j  < 
V ,  j ,  ( j  -  1 ) )  +  1 ) ) )
291290eqeq2d 2481 . . . . . . . . . . . . . 14  |-  ( ( j  -  1 )  =  if ( j  <  V ,  j ,  ( j  - 
1 ) )  -> 
( j  =  if ( ( j  - 
1 )  <  V ,  ( j  - 
1 ) ,  ( ( j  -  1 )  +  1 ) )  <->  j  =  if ( if ( j  <  V ,  j ,  ( j  - 
1 ) )  < 
V ,  if ( j  <  V , 
j ,  ( j  -  1 ) ) ,  ( if ( j  <  V , 
j ,  ( j  -  1 ) )  +  1 ) ) ) )
292 iftrue 3878 . . . . . . . . . . . . . . . 16  |-  ( j  <  V  ->  if ( j  <  V ,  j ,  ( j  +  1 ) )  =  j )
293292eqcomd 2477 . . . . . . . . . . . . . . 15  |-  ( j  <  V  ->  j  =  if ( j  < 
V ,  j ,  ( j  +  1 ) ) )
294293adantl 473 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  /\  j  <  V )  -> 
j  =  if ( j  <  V , 
j ,  ( j  +  1 ) ) )
295 zlem1lt 11012 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ZZ  /\  V  e.  ZZ )  ->  ( j  <_  V  <->  ( j  -  1 )  <  V ) )
296239, 199, 295syl2anr 486 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  -> 
( j  <_  V  <->  ( j  -  1 )  <  V ) )
297259necomd 2698 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( ( 0 ... N )  \  { V } )  ->  V  =/=  j )
298297adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( ( 0 ... N )  \  { V } ) )  ->  V  =/=  j )
299 ltlen 9753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  RR  /\  V  e.  RR )  ->