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

Theorem poimirlem23 32009
Description: Lemma for poimir 32019, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimirlem23.1  |-  ( ph  ->  T : ( 1 ... N ) --> ( 0..^ K ) )
poimirlem23.2  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem23.3  |-  ( ph  ->  V  e.  ( 0 ... N ) )
Assertion
Ref Expression
poimirlem23  |-  ( ph  ->  ( 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  <->  -.  ( V  =  N  /\  ( ( T `  N )  =  0  /\  ( U `  N )  =  N ) ) ) )
Distinct variable groups:    j, p, y, ph    j, N, y    T, j, y    U, j, y    j, V, y    ph, p    j, K, p    N, p    T, p    U, p    y, K    V, p

Proof of Theorem poimirlem23
StepHypRef Expression
1 ovex 6348 . . . . . 6  |-  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
21csbex 4554 . . . . 5  |-  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  e. 
_V
32rgenw 2761 . . . 4  |-  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
4 eqid 2462 . . . . 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 } ) ) ) )
5 fveq1 5891 . . . . . . 7  |-  ( p  =  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  ->  ( p `  N )  =  (
[_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N ) )
65neeq1d 2695 . . . . . 6  |-  ( p  =  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  ->  ( (
p `  N )  =/=  0  <->  ( [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =/=  0
) )
7 df-ne 2635 . . . . . 6  |-  ( (
[_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =/=  0  <->  -.  ( [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) `  N )  =  0 )
86, 7syl6bb 269 . . . . 5  |-  ( p  =  [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  ->  ( (
p `  N )  =/=  0  <->  -.  ( [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0 ) )
94, 8rexrnmpt 6060 . . . 4  |-  ( 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. 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  <->  E. 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 } ) ) ) `  N )  =  0 ) )
103, 9ax-mp 5 . . 3  |-  ( 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  <->  E. 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 } ) ) ) `  N )  =  0 )
11 rexnal 2848 . . 3  |-  ( E. 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 } ) ) ) `  N )  =  0  <->  -.  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 } ) ) ) `  N )  =  0 )
1210, 11bitri 257 . 2  |-  ( 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  <->  -.  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 } ) ) ) `  N )  =  0 )
13 poimir.0 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  NN )
1413nnzd 11073 . . . . . . . . . 10  |-  ( ph  ->  N  e.  ZZ )
15 poimirlem23.3 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  ( 0 ... N ) )
16 elfzelz 11835 . . . . . . . . . . 11  |-  ( V  e.  ( 0 ... N )  ->  V  e.  ZZ )
1715, 16syl 17 . . . . . . . . . 10  |-  ( ph  ->  V  e.  ZZ )
18 zlem1lt 11022 . . . . . . . . . 10  |-  ( ( N  e.  ZZ  /\  V  e.  ZZ )  ->  ( N  <_  V  <->  ( N  -  1 )  <  V ) )
1914, 17, 18syl2anc 671 . . . . . . . . 9  |-  ( ph  ->  ( N  <_  V  <->  ( N  -  1 )  <  V ) )
20 elfzle2 11838 . . . . . . . . . . 11  |-  ( V  e.  ( 0 ... N )  ->  V  <_  N )
2115, 20syl 17 . . . . . . . . . 10  |-  ( ph  ->  V  <_  N )
2217zred 11074 . . . . . . . . . . . 12  |-  ( ph  ->  V  e.  RR )
2313nnred 10657 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  RR )
2422, 23letri3d 9808 . . . . . . . . . . 11  |-  ( ph  ->  ( V  =  N  <-> 
( V  <_  N  /\  N  <_  V ) ) )
2524biimprd 231 . . . . . . . . . 10  |-  ( ph  ->  ( ( V  <_  N  /\  N  <_  V
)  ->  V  =  N ) )
2621, 25mpand 686 . . . . . . . . 9  |-  ( ph  ->  ( N  <_  V  ->  V  =  N ) )
2719, 26sylbird 243 . . . . . . . 8  |-  ( ph  ->  ( ( N  - 
1 )  <  V  ->  V  =  N ) )
2827necon3ad 2649 . . . . . . 7  |-  ( ph  ->  ( V  =/=  N  ->  -.  ( N  - 
1 )  <  V
) )
29 nnm1nn0 10945 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
3013, 29syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
31 nn0fz0 11925 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  NN0  <->  ( N  - 
1 )  e.  ( 0 ... ( N  -  1 ) ) )
3230, 31sylib 201 . . . . . . . . . . 11  |-  ( ph  ->  ( N  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
3332adantr 471 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  -> 
( N  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
34 iffalse 3902 . . . . . . . . . . . . . . . 16  |-  ( -.  ( N  -  1 )  <  V  ->  if ( ( N  - 
1 )  <  V ,  ( N  - 
1 ) ,  ( ( N  -  1 )  +  1 ) )  =  ( ( N  -  1 )  +  1 ) )
3513nncnd 10658 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  CC )
36 npcan1 10077 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
3735, 36syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
3834, 37sylan9eqr 2518 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  ->  if ( ( N  - 
1 )  <  V ,  ( N  - 
1 ) ,  ( ( N  -  1 )  +  1 ) )  =  N )
3938csbeq1d 3382 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  ->  [_ if ( ( N  -  1 )  < 
V ,  ( N  -  1 ) ,  ( ( N  - 
1 )  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  = 
[_ N  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
40 oveq2 6328 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  N  ->  (
1 ... j )  =  ( 1 ... N
) )
4140imaeq2d 5190 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  N  ->  ( U " ( 1 ... j ) )  =  ( U " (
1 ... N ) ) )
4241xpeq1d 4879 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  N  ->  (
( U " (
1 ... j ) )  X.  { 1 } )  =  ( ( U " ( 1 ... N ) )  X.  { 1 } ) )
43 oveq1 6327 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  N  ->  (
j  +  1 )  =  ( N  + 
1 ) )
4443oveq1d 6335 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  N  ->  (
( j  +  1 ) ... N )  =  ( ( N  +  1 ) ... N ) )
4544imaeq2d 5190 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  N  ->  ( U " ( ( j  +  1 ) ... N ) )  =  ( U " (
( N  +  1 ) ... N ) ) )
4645xpeq1d 4879 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  N  ->  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( U " (
( N  +  1 ) ... N ) )  X.  { 0 } ) )
4742, 46uneq12d 3601 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  N  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )  =  ( ( ( U " ( 1 ... N ) )  X.  { 1 } )  u.  ( ( U " ( ( N  +  1 ) ... N ) )  X.  { 0 } ) ) )
48 poimirlem23.2 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
49 f1ofo 5848 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U :
( 1 ... N
) -onto-> ( 1 ... N ) )
50 foima 5825 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N )  -> 
( U " (
1 ... N ) )  =  ( 1 ... N ) )
5148, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( 1 ... N ) )
5251xpeq1d 4879 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  X.  {
1 } )  =  ( ( 1 ... N )  X.  {
1 } ) )
5323ltp1d 10570 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  N  <  ( N  +  1 ) )
5414peano2zd 11077 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
55 fzn 11850 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( N  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  <  ( N  +  1 )  <-> 
( ( N  + 
1 ) ... N
)  =  (/) ) )
5654, 14, 55syl2anc 671 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( N  <  ( N  +  1 )  <-> 
( ( N  + 
1 ) ... N
)  =  (/) ) )
5753, 56mpbid 215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( N  + 
1 ) ... N
)  =  (/) )
5857imaeq2d 5190 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( U " (
( N  +  1 ) ... N ) )  =  ( U
" (/) ) )
5958xpeq1d 4879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( U "
( ( N  + 
1 ) ... N
) )  X.  {
0 } )  =  ( ( U " (/) )  X.  { 0 } ) )
60 ima0 5205 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U
" (/) )  =  (/)
6160xpeq1i 4876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( U " (/) )  X. 
{ 0 } )  =  ( (/)  X.  {
0 } )
62 0xp 4937 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (/)  X. 
{ 0 } )  =  (/)
6361, 62eqtri 2484 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( U " (/) )  X. 
{ 0 } )  =  (/)
6459, 63syl6eq 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( U "
( ( N  + 
1 ) ... N
) )  X.  {
0 } )  =  (/) )
6552, 64uneq12d 3601 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( U
" ( 1 ... N ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( N  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( 1 ... N
)  X.  { 1 } )  u.  (/) ) )
66 un0 3771 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1 ... N
)  X.  { 1 } )  u.  (/) )  =  ( ( 1 ... N )  X.  {
1 } )
6765, 66syl6eq 2512 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( U
" ( 1 ... N ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( N  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( 1 ... N )  X.  { 1 } ) )
6847, 67sylan9eqr 2518 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  =  N )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )  =  ( ( 1 ... N )  X. 
{ 1 } ) )
6968oveq2d 6336 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  =  N )  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( T  oF  +  ( ( 1 ... N
)  X.  { 1 } ) ) )
7013, 69csbied 3402 . . . . . . . . . . . . . . 15  |-  ( ph  ->  [_ N  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  =  ( T  oF  +  ( ( 1 ... N )  X. 
{ 1 } ) ) )
7170adantr 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  ->  [_ N  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  =  ( T  oF  +  ( ( 1 ... N )  X. 
{ 1 } ) ) )
7239, 71eqtrd 2496 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  ->  [_ if ( ( N  -  1 )  < 
V ,  ( N  -  1 ) ,  ( ( N  - 
1 )  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  =  ( T  oF  +  ( ( 1 ... N )  X. 
{ 1 } ) ) )
7372fveq1d 5894 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  -> 
( [_ if ( ( N  -  1 )  <  V ,  ( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  ( ( T  oF  +  ( ( 1 ... N )  X. 
{ 1 } ) ) `  N ) )
74 elfzonn0 11997 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0..^ K )  ->  j  e.  NN0 )
75 nn0p1nn 10943 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  NN )
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0..^ K )  ->  ( j  +  1 )  e.  NN )
77 elsni 4005 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  { 1 }  ->  y  =  1 )
7877oveq2d 6336 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  { 1 }  ->  ( j  +  y )  =  ( j  +  1 ) )
7978eleq1d 2524 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  { 1 }  ->  ( ( j  +  y )  e.  NN  <->  ( j  +  1 )  e.  NN ) )
8076, 79syl5ibrcom 230 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0..^ K )  ->  ( y  e.  { 1 }  ->  ( j  +  y )  e.  NN ) )
8180imp 435 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0..^ K )  /\  y  e.  { 1 } )  ->  ( j  +  y )  e.  NN )
8281adantl 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( j  e.  ( 0..^ K )  /\  y  e.  {
1 } ) )  ->  ( j  +  y )  e.  NN )
83 poimirlem23.1 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T : ( 1 ... N ) --> ( 0..^ K ) )
84 1ex 9669 . . . . . . . . . . . . . . . . 17  |-  1  e.  _V
8584fconst 5796 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... N )  X.  { 1 } ) : ( 1 ... N ) --> { 1 }
8685a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1 ... N )  X.  {
1 } ) : ( 1 ... N
) --> { 1 } )
87 ovex 6348 . . . . . . . . . . . . . . . 16  |-  ( 1 ... N )  e. 
_V
8887a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... N
)  e.  _V )
89 inidm 3653 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
9082, 83, 86, 88, 88, 89off 6578 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  oF  +  ( ( 1 ... N )  X. 
{ 1 } ) ) : ( 1 ... N ) --> NN )
91 elfz1end 11864 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  <->  N  e.  ( 1 ... N
) )
9213, 91sylib 201 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  ( 1 ... N ) )
9390, 92ffvelrnd 6051 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( T  oF  +  ( (
1 ... N )  X. 
{ 1 } ) ) `  N )  e.  NN )
9493adantr 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  -> 
( ( T  oF  +  ( (
1 ... N )  X. 
{ 1 } ) ) `  N )  e.  NN )
9573, 94eqeltrd 2540 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  -> 
( [_ if ( ( N  -  1 )  <  V ,  ( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  e.  NN )
9695nnne0d 10687 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  -> 
( [_ if ( ( N  -  1 )  <  V ,  ( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =/=  0
)
97 breq1 4421 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( N  - 
1 )  ->  (
y  <  V  <->  ( N  -  1 )  < 
V ) )
98 id 22 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( N  - 
1 )  ->  y  =  ( N  - 
1 ) )
99 oveq1 6327 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( N  - 
1 )  ->  (
y  +  1 )  =  ( ( N  -  1 )  +  1 ) )
10097, 98, 99ifbieq12d 3920 . . . . . . . . . . . . . . 15  |-  ( y  =  ( N  - 
1 )  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  =  if ( ( N  -  1 )  <  V , 
( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) ) )
101100csbeq1d 3382 . . . . . . . . . . . . . 14  |-  ( y  =  ( N  - 
1 )  ->  [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  = 
[_ if ( ( N  -  1 )  <  V ,  ( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
102101fveq1d 5894 . . . . . . . . . . . . 13  |-  ( y  =  ( N  - 
1 )  ->  ( [_ if ( y  < 
V ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  (
[_ if ( ( N  -  1 )  <  V ,  ( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N ) )
103102neeq1d 2695 . . . . . . . . . . . 12  |-  ( y  =  ( N  - 
1 )  ->  (
( [_ if ( y  <  V ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =/=  0  <->  (
[_ if ( ( N  -  1 )  <  V ,  ( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =/=  0
) )
1047, 103syl5bbr 267 . . . . . . . . . . 11  |-  ( y  =  ( N  - 
1 )  ->  ( -.  ( [_ if ( y  <  V , 
y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) `  N )  =  0  <->  ( [_ if ( ( N  - 
1 )  <  V ,  ( N  - 
1 ) ,  ( ( N  -  1 )  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =/=  0
) )
105104rspcev 3162 . . . . . . . . . 10  |-  ( ( ( N  -  1 )  e.  ( 0 ... ( N  - 
1 ) )  /\  ( [_ if ( ( N  -  1 )  <  V ,  ( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =/=  0
)  ->  E. 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 } ) ) ) `  N )  =  0 )
10633, 96, 105syl2anc 671 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  ->  E. 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 } ) ) ) `  N )  =  0 )
107106, 11sylib 201 . . . . . . . 8  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  ->  -.  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 } ) ) ) `  N )  =  0 )
108107ex 440 . . . . . . 7  |-  ( ph  ->  ( -.  ( N  -  1 )  < 
V  ->  -.  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 } ) ) ) `  N )  =  0 ) )
10928, 108syld 45 . . . . . 6  |-  ( ph  ->  ( V  =/=  N  ->  -.  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 } ) ) ) `  N )  =  0 ) )
110109necon4ad 2655 . . . . 5  |-  ( ph  ->  ( 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 } ) ) ) `  N )  =  0  ->  V  =  N ) )
111110pm4.71rd 645 . . . 4  |-  ( ph  ->  ( 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 } ) ) ) `  N )  =  0  <-> 
( V  =  N  /\  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 } ) ) ) `  N )  =  0 ) ) )
11230nn0zd 11072 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
113 uzid 11207 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
114 peano2uz 11246 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
115112, 113, 1143syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
11637, 115eqeltrrd 2541 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
117 fzss2 11873 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... N
) )
118116, 117syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
119118sselda 3444 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  j  e.  ( 0 ... N
) )
12092adantr 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  N  e.  ( 1 ... N
) )
121 ffn 5755 . . . . . . . . . . . . . . 15  |-  ( T : ( 1 ... N ) --> ( 0..^ K )  ->  T  Fn  ( 1 ... N
) )
12283, 121syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  T  Fn  ( 1 ... N ) )
123122adantr 471 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  T  Fn  ( 1 ... N
) )
12484fconst 5796 . . . . . . . . . . . . . . . . 17  |-  ( ( U " ( 1 ... j ) )  X.  { 1 } ) : ( U
" ( 1 ... j ) ) --> { 1 }
125 c0ex 9668 . . . . . . . . . . . . . . . . . 18  |-  0  e.  _V
126125fconst 5796 . . . . . . . . . . . . . . . . 17  |-  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( U
" ( ( j  +  1 ) ... N ) ) --> { 0 }
127124, 126pm3.2i 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( U " (
1 ... j ) )  X.  { 1 } ) : ( U
" ( 1 ... j ) ) --> { 1 }  /\  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } ) : ( U " ( ( j  +  1 ) ... N ) ) --> { 0 } )
128 dff1o3 5847 . . . . . . . . . . . . . . . . . . 19  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( U :
( 1 ... N
) -onto-> ( 1 ... N )  /\  Fun  `' U ) )
129128simprbi 470 . . . . . . . . . . . . . . . . . 18  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' U
)
130 imain 5685 . . . . . . . . . . . . . . . . . 18  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... j
) )  i^i  ( U " ( ( j  +  1 ) ... N ) ) ) )
13148, 129, 1303syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U " (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) ) )  =  ( ( U " ( 1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) ) )
132 elfzelz 11835 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0 ... N )  ->  j  e.  ZZ )
133132zred 11074 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
134133ltp1d 10570 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... N )  ->  j  <  ( j  +  1 ) )
135 fzdisj 11861 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  <  ( j  +  1 )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
136134, 135syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... N )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
137136imaeq2d 5190 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  ( U " (/) ) )
138137, 60syl6eq 2512 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  (/) )
139131, 138sylan9req 2517 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( U " (
1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) )  =  (/) )
140 fun 5773 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( 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 } ) )
141127, 139, 140sylancr 674 . . . . . . . . . . . . . . 15  |-  ( (
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 } ) )
142 elfznn0 11922 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0 ... N )  ->  j  e.  NN0 )
143142, 75syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  NN )
144 nnuz 11228 . . . . . . . . . . . . . . . . . . . . 21  |-  NN  =  ( ZZ>= `  1 )
145143, 144syl6eleq 2550 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
146 elfzuz3 11832 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  j )
)
147 fzsplit2 11859 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  j )
)  ->  ( 1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
148145, 146, 147syl2anc 671 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... N )  ->  (
1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
149148imaeq2d 5190 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( 1 ... N ) )  =  ( U " (
( 1 ... j
)  u.  ( ( j  +  1 ) ... N ) ) ) )
150 imaundi 5270 . . . . . . . . . . . . . . . . . 18  |-  ( U
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... j
) )  u.  ( U " ( ( j  +  1 ) ... N ) ) )
151149, 150syl6req 2513 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... N )  ->  (
( U " (
1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... N
) ) )  =  ( U " (
1 ... N ) ) )
152151, 51sylan9eqr 2518 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( U " (
1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... N
) ) )  =  ( 1 ... N
) )
153152feq2d 5741 . . . . . . . . . . . . . . 15  |-  ( (
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 } ) ) )
154141, 153mpbid 215 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  {
0 } ) )
155 ffn 5755 . . . . . . . . . . . . . 14  |-  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  {
0 } )  -> 
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( 1 ... N ) )
156154, 155syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )  Fn  ( 1 ... N ) )
15787a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
1 ... N )  e. 
_V )
158 eqidd 2463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  N  e.  ( 1 ... N
) )  ->  ( T `  N )  =  ( T `  N ) )
159 eqidd 2463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  N  e.  ( 1 ... N
) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  =  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
) )
160123, 156, 157, 157, 89, 158, 159ofval 6572 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  N  e.  ( 1 ... N
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  ( ( T `  N
)  +  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N ) ) )
161120, 160mpdan 679 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  ( ( T `  N
)  +  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N ) ) )
162161eqeq1d 2464 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0  <-> 
( ( T `  N )  +  ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N ) )  =  0 ) )
16383, 92ffvelrnd 6051 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T `  N
)  e.  ( 0..^ K ) )
164 elfzonn0 11997 . . . . . . . . . . . . . 14  |-  ( ( T `  N )  e.  ( 0..^ K )  ->  ( T `  N )  e.  NN0 )
165163, 164syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( T `  N
)  e.  NN0 )
166165nn0red 10960 . . . . . . . . . . . 12  |-  ( ph  ->  ( T `  N
)  e.  RR )
167166adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( T `  N )  e.  RR )
168165nn0ge0d 10962 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( T `  N ) )
169168adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  0  <_  ( T `  N
) )
170 1re 9673 . . . . . . . . . . . . . 14  |-  1  e.  RR
171 snssi 4129 . . . . . . . . . . . . . 14  |-  ( 1  e.  RR  ->  { 1 }  C_  RR )
172170, 171ax-mp 5 . . . . . . . . . . . . 13  |-  { 1 }  C_  RR
173 0re 9674 . . . . . . . . . . . . . 14  |-  0  e.  RR
174 snssi 4129 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  { 0 }  C_  RR )
175173, 174ax-mp 5 . . . . . . . . . . . . 13  |-  { 0 }  C_  RR
176172, 175unssi 3621 . . . . . . . . . . . 12  |-  ( { 1 }  u.  {
0 } )  C_  RR
177154, 120ffvelrnd 6051 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  ( { 1 }  u.  { 0 } ) )
178176, 177sseldi 3442 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  RR )
179 elun 3586 . . . . . . . . . . . . 13  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  ( { 1 }  u.  { 0 } )  <->  ( (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  { 1 }  \/  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  e.  { 0 } ) )
180 0le1 10170 . . . . . . . . . . . . . . 15  |-  0  <_  1
181 elsni 4005 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  { 1 }  ->  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  1 )
182180, 181syl5breqr 4455 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  { 1 }  ->  0  <_  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N ) )
183 0le0 10732 . . . . . . . . . . . . . . 15  |-  0  <_  0
184 elsni 4005 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  { 0 }  ->  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  0 )
185183, 184syl5breqr 4455 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  { 0 }  ->  0  <_  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N ) )
186182, 185jaoi 385 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  e.  { 1 }  \/  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N )  e. 
{ 0 } )  ->  0  <_  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N ) )
187179, 186sylbi 200 . . . . . . . . . . . 12  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  ( { 1 }  u.  { 0 } )  ->  0  <_  ( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
) )
188177, 187syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  0  <_  ( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
) )
189 add20 10159 . . . . . . . . . . 11  |-  ( ( ( ( T `  N )  e.  RR  /\  0  <_  ( T `  N ) )  /\  ( ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  e.  RR  /\  0  <_  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
) ) )  -> 
( ( ( T `
 N )  +  ( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
) )  =  0  <-> 
( ( T `  N )  =  0  /\  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  0 ) ) )
190167, 169, 178, 188, 189syl22anc 1277 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( T `  N )  +  ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N ) )  =  0  <->  (
( T `  N
)  =  0  /\  ( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  0 ) ) )
191162, 190bitrd 261 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0  <-> 
( ( T `  N )  =  0  /\  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  0 ) ) )
192119, 191syldan 477 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0  <-> 
( ( T `  N )  =  0  /\  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  0 ) ) )
193192ralbidva 2836 . . . . . . 7  |-  ( ph  ->  ( A. j  e.  ( 0 ... ( N  -  1 ) ) ( ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) ) `  N )  =  0  <->  A. j  e.  ( 0 ... ( N  -  1 ) ) ( ( T `
 N )  =  0  /\  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N )  =  0 ) ) )
194193adantr 471 . . . . . 6  |-  ( (
ph  /\  V  =  N )  ->  ( A. j  e.  (
0 ... ( N  - 
1 ) ) ( ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0  <->  A. j  e.  (
0 ... ( N  - 
1 ) ) ( ( T `  N
)  =  0  /\  ( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  0 ) ) )
195 breq2 4422 . . . . . . . . . . . . . 14  |-  ( V  =  N  ->  (
y  <  V  <->  y  <  N ) )
196195ifbid 3915 . . . . . . . . . . . . 13  |-  ( V  =  N  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  =  if ( y  <  N , 
y ,  ( y  +  1 ) ) )
197 elfzelz 11835 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  ZZ )
198197zred 11074 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  RR )
199198adantl 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  e.  RR )
20030nn0red 10960 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  e.  RR )
201200adantr 471 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
20223adantr 471 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  RR )
203 elfzle2 11838 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  <_  ( N  -  1 ) )
204203adantl 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <_  ( N  -  1 ) )
20523ltm1d 10572 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  <  N )
206205adantr 471 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
207199, 201, 202, 204, 206lelttrd 9824 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <  N )
208207iftrued 3901 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  if ( y  <  N ,  y ,  ( y  +  1 ) )  =  y )
209196, 208sylan9eqr 2518 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  V  =  N )  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  =  y )
210209an32s 818 . . . . . . . . . . 11  |-  ( ( ( ph  /\  V  =  N )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  =  y )
211210csbeq1d 3382 . . . . . . . . . 10  |-  ( ( ( ph  /\  V  =  N )  /\  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  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
212211fveq1d 5894 . . . . . . . . 9  |-  ( ( ( ph  /\  V  =  N )  /\  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 } ) ) ) `  N )  =  (
[_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N ) )
213212eqeq1d 2464 . . . . . . . 8  |-  ( ( ( ph  /\  V  =  N )  /\  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 } ) ) ) `  N )  =  0  <-> 
( [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0 ) )
214213ralbidva 2836 . . . . . . 7  |-  ( (
ph  /\  V  =  N )  ->  ( 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 } ) ) ) `  N )  =  0  <->  A. y  e.  (
0 ... ( N  - 
1 ) ) (
[_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0 ) )
215 nfv 1772 . . . . . . . 8  |-  F/ y ( ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0
216 nfcsb1v 3391 . . . . . . . . . 10  |-  F/_ j [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )
217 nfcv 2603 . . . . . . . . . 10  |-  F/_ j N
218216, 217nffv 5899 . . . . . . . . 9  |-  F/_ j
( [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )
219218nfeq1 2616 . . . . . . . 8  |-  F/ j ( [_ y  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0
220 csbeq1a 3384 . . . . . . . . . 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 } ) ) ) )
221220fveq1d 5894 . . . . . . . . 9  |-  ( j  =  y  ->  (
( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  (
[_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N ) )
222221eqeq1d 2464 . . . . . . . 8  |-  ( j  =  y  ->  (
( ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0  <-> 
( [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0 ) )
223215, 219, 222cbvral 3027 . . . . . . 7  |-  ( A. j  e.  ( 0 ... ( N  - 
1 ) ) ( ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0  <->  A. y  e.  (
0 ... ( N  - 
1 ) ) (
[_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0 )
224214, 223syl6bbr 271 . . . . . 6  |-  ( (
ph  /\  V  =  N )  ->  ( 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 } ) ) ) `  N )  =  0  <->  A. j  e.  (
0 ... ( N  - 
1 ) ) ( ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0 ) )
225 ne0i 3749 . . . . . . . . . 10  |-  ( ( N  -  1 )  e.  ( 0 ... ( N  -  1 ) )  ->  (
0 ... ( N  - 
1 ) )  =/=  (/) )
226 r19.3rzv 3874 . . . . . . . . . 10  |-  ( ( 0 ... ( N  -  1 ) )  =/=  (/)  ->  ( ( T `  N )  =  0  <->  A. j  e.  ( 0 ... ( N  -  1 ) ) ( T `  N )  =  0 ) )
22732, 225, 2263syl 18 . . . . . . . . 9  |-  ( ph  ->  ( ( T `  N )  =  0  <->  A. j  e.  (
0 ... ( N  - 
1 ) ) ( T `  N )  =  0 ) )
228 elfzelz 11835 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  j  e.  ZZ )
229228zred 11074 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  j  e.  RR )
230229ltp1d 10570 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  j  <  ( j  +  1 ) )
231230, 135syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
232231imaeq2d 5190 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  ( U " (/) ) )
233232, 60syl6eq 2512 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  (/) )
234131, 233sylan9req 2517 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( U " (
1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) )  =  (/) )
235234adantlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( U " (
1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) )  =  (/) )
236 simplr 767 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( U `  N )  =  N )
237 f1ofn 5842 . . . . . . . . . . . . . . . . . . 19  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U  Fn  ( 1 ... N
) )
23848, 237syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U  Fn  ( 1 ... N ) )
239238adantr 471 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  U  Fn  ( 1 ... N
) )
240 elfznn0 11922 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  j  e.  NN0 )
241240, 75syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  (
j  +  1 )  e.  NN )
242241, 144syl6eleq 2550 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
243 fzss1 11872 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  +  1 )  e.  ( ZZ>= `  1
)  ->  ( (
j  +  1 ) ... N )  C_  ( 1 ... N
) )
244242, 243syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  (
( j  +  1 ) ... N ) 
C_  ( 1 ... N ) )
245244adantl 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( j  +  1 ) ... N ) 
C_  ( 1 ... N ) )
24637adantr 471 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  =  N )
247 elfzuz3 11832 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  ( ZZ>= `  j
) )
248 eluzp1p1 11218 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  -  1 )  e.  ( ZZ>= `  j
)  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( j  +  1 ) ) )
249247, 248syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  (
j  +  1 ) ) )
250249adantl 472 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  (
j  +  1 ) ) )
251246, 250eqeltrrd 2541 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  ( j  +  1 ) ) )
252 eluzfz2 11842 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( ZZ>= `  (
j  +  1 ) )  ->  N  e.  ( ( j  +  1 ) ... N
) )
253251, 252syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ( j  +  1 ) ... N
) )
254 fnfvima 6173 . . . . . . . . . . . . . . . . 17  |-  ( ( U  Fn  ( 1 ... N )  /\  ( ( j  +  1 ) ... N
)  C_  ( 1 ... N )  /\  N  e.  ( (
j  +  1 ) ... N ) )  ->  ( U `  N )  e.  ( U " ( ( j  +  1 ) ... N ) ) )
255239, 245, 253, 254syl3anc 1276 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( U `  N )  e.  ( U " (
( j  +  1 ) ... N ) ) )
256255adantlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( U `  N )  e.  ( U " (
( j  +  1 ) ... N ) ) )
257236, 256eqeltrrd 2541 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( U " (
( j  +  1 ) ... N ) ) )
258 fnconstg 5798 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  _V  ->  (
( U " (
1 ... j ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... j ) ) )
25984, 258ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( U " ( 1 ... j ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... j ) )
260 fnconstg 5798 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  _V  ->  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U " ( ( j  +  1 ) ... N ) ) )
261125, 260ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U
" ( ( j  +  1 ) ... N ) )
262 fvun2 5965 . . . . . . . . . . . . . . 15  |-  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  Fn  ( U " (
1 ... j ) )  /\  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( U "
( ( j  +  1 ) ... N
) )  /\  (
( ( U "
( 1 ... j
) )  i^i  ( U " ( ( j  +  1 ) ... N ) ) )  =  (/)  /\  N  e.  ( U " (
( j  +  1 ) ... N ) ) ) )  -> 
( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  ( ( ( U " (
( j  +  1 ) ... N ) )  X.  { 0 } ) `  N
) )
263259, 261, 262mp3an12 1363 . . . . . . . . . . . . . 14  |-  ( ( ( ( U "
( 1 ... j
) )  i^i  ( U " ( ( j  +  1 ) ... N ) ) )  =  (/)  /\  N  e.  ( U " (
( j  +  1 ) ... N ) ) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  =  ( ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) `  N ) )
264235, 257, 263syl2anc 671 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  =  ( ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) `  N ) )
265125fvconst2 6149 . . . . . . . . . . . . . 14  |-  ( N  e.  ( U "
( ( j  +  1 ) ... N
) )  ->  (
( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) `  N )  =  0 )
266257, 265syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) `  N )  =  0 )
267264, 266eqtrd 2496 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  =  0 )
268267ralrimiva 2814 . . . . . . . . . . 11  |-  ( (
ph  /\  ( U `  N )  =  N )  ->  A. j  e.  ( 0 ... ( N  -  1 ) ) ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  0 )
269268ex 440 . . . . . . . . . 10  |-  ( ph  ->  ( ( U `  N )  =  N  ->  A. j  e.  ( 0 ... ( N  -  1 ) ) ( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  N
)  =  0 ) )
27032adantr 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( N  -  1 )  e.  ( 0 ... ( N  -  1 ) ) )
271 ax-1ne0 9639 . . . . . . . . . . . . . . 15  |-  1  =/=  0
272 imain 5685 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... ( N  - 
1 ) )  i^i  ( ( ( N  -  1 )  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... ( N  -  1 ) ) )  i^i  ( U " ( ( ( N  -  1 )  +  1 ) ... N ) ) ) )
27348, 129, 2723syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... ( N  -  1 ) )  i^i  ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  ( ( U " ( 1 ... ( N  - 
1 ) ) )  i^i  ( U "
( ( ( N  -  1 )  +  1 ) ... N
) ) ) )
274205, 37breqtrrd 4445 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( N  -  1 )  <  ( ( N  -  1 )  +  1 ) )
275 fzdisj 11861 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  -  1 )  <  ( ( N  -  1 )  +  1 )  ->  (
( 1 ... ( N  -  1 ) )  i^i  ( ( ( N  -  1 )  +  1 ) ... N ) )  =  (/) )
276274, 275syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1 ... ( N  -  1 ) )  i^i  (
( ( N  - 
1 )  +  1 ) ... N ) )  =  (/) )
277276imaeq2d 5190 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... ( N  -  1 ) )  i^i  ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  ( U
" (/) ) )
278277, 60syl6eq 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... ( N  -  1 ) )  i^i  ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  (/) )
279273, 278eqtr3d 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... ( N  -  1 ) ) )  i^i  ( U " ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  (/) )
280279adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( ( U " ( 1 ... ( N  -  1 ) ) )  i^i  ( U " (
( ( N  - 
1 )  +  1 ) ... N ) ) )  =  (/) )
28192adantr 471 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  N  e.  ( 1 ... N
) )
282 elimasni 5217 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( U " { N } )  ->  N U N )
283 fnbrfvb 5932 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( U  Fn  ( 1 ... N )  /\  N  e.  ( 1 ... N ) )  ->  ( ( U `
 N )  =  N  <->  N U N ) )
284238, 92, 283syl2anc 671 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( U `  N )  =  N  <-> 
N U N ) )
285282, 284syl5ibr 229 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( N  e.  ( U " { N } )  ->  ( U `  N )  =  N ) )
286285necon3ad 2649 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( U `  N )  =/=  N  ->  -.  N  e.  ( U " { N } ) ) )
287286imp 435 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  -.  N  e.  ( U " { N } ) )
288281, 287eldifd 3427 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  N  e.  ( ( 1 ... N )  \  ( U " { N }
) ) )
289 imadif 5684 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... N )  \  { N } ) )  =  ( ( U
" ( 1 ... N ) )  \ 
( U " { N } ) ) )
29048, 129, 2893syl 18 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { N } ) )  =  ( ( U "
( 1 ... N
) )  \  ( U " { N }
) ) )
291 difun2 3859 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... ( N  -  1 ) )  u.  { N } )  \  { N } )  =  ( ( 1 ... ( N  -  1 ) )  \  { N } )
29213, 144syl6eleq 2550 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
293 fzm1 11909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  1
)  ->  ( j  e.  ( 1 ... N
)  <->  ( j  e.  ( 1 ... ( N  -  1 ) )  \/  j  =  N ) ) )
294292, 293syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( j  e.  ( 1 ... N )  <-> 
( j  e.  ( 1 ... ( N  -  1 ) )  \/  j  =  N ) ) )
295 elun 3586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( ( 1 ... ( N  - 
1 ) )  u. 
{ N } )  <-> 
( j  e.  ( 1 ... ( N  -  1 ) )  \/  j  e.  { N } ) )
296 elsn 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  { N }  <->  j  =  N )
297296orbi2i 526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  ( 1 ... ( N  - 
1 ) )  \/  j  e.  { N } )  <->  ( j  e.  ( 1 ... ( N  -  1 ) )  \/  j  =  N ) )
298295, 297bitri 257 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  e.  ( ( 1 ... ( N  - 
1 ) )  u. 
{ N } )  <-> 
( j  e.  ( 1 ... ( N  -  1 ) )  \/  j  =  N ) )
299294, 298syl6rbbr 272 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( j  e.  ( ( 1 ... ( N  -  1 ) )  u.  { N } )  <->  j  e.  ( 1 ... N
) ) )
300299eqrdv 2460 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( 1 ... ( N  -  1 ) )  u.  { N } )  =  ( 1 ... N ) )
301300difeq1d 3562 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( 1 ... ( N  - 
1 ) )  u. 
{ N } ) 
\  { N }
)  =  ( ( 1 ... N ) 
\  { N }
) )
302200, 23ltnled 9813 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( N  - 
1 )  <  N  <->  -.  N  <_  ( N  -  1 ) ) )
303205, 302mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  -.  N  <_  ( N  -  1 ) )
304 elfzle2 11838 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  <_  ( N  -  1 ) )
305303, 304nsyl 126 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  -.  N  e.  ( 1 ... ( N  -  1 ) ) )
306 difsn 4119 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  N  e.  ( 1 ... ( N  - 
1 ) )  -> 
( ( 1 ... ( N  -  1 ) )  \  { N } )  =  ( 1 ... ( N  -  1 ) ) )
307305, 306syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( 1 ... ( N  -  1 ) )  \  { N } )  =  ( 1 ... ( N  -  1 ) ) )
308291, 301, 3073eqtr3a 2520 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1 ... N )  \  { N } )  =  ( 1 ... ( N  -  1 ) ) )
309308imaeq2d 5190 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { N } ) )  =  ( U " (
1 ... ( N  - 
1 ) ) ) )
31051difeq1d 3562 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { N }
) )  =  ( ( 1 ... N
)  \  ( U " { N } ) ) )
311290, 309, 3103eqtr3rd 2505 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( 1 ... N )  \  ( U " { N }
) )  =  ( U " ( 1 ... ( N  - 
1 ) ) ) )
312311adantr 471 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
1 ... N )  \ 
( U " { N } ) )  =  ( U " (
1 ... ( N  - 
1 ) ) ) )
313288, 312eleqtrd 2542 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  N  e.  ( U " ( 1 ... ( N  - 
1 ) ) ) )
314 fnconstg 5798 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  e.  _V  ->  (
( U " (
1 ... ( N  - 
1 ) ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... ( N  -  1 ) ) ) )
31584, 314ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U " ( 1 ... ( N  - 
1 ) ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... ( N  -  1 ) ) )
316 fnconstg 5798 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  _V  ->  (
( U " (
( ( N  - 
1 )  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U " ( ( ( N  -  1 )  +  1 ) ... N ) ) )
317125, 316ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U " ( ( ( N  -  1 )  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U
" ( ( ( N  -  1 )  +  1 ) ... N ) )
318 fvun1 5964 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( U "
( 1 ... ( N  -  1 ) ) )  X.  {
1 } )  Fn  ( U " (
1 ... ( N  - 
1 ) ) )  /\  ( ( U
" ( ( ( N  -  1 )  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( U "
( ( ( N  -  1 )  +  1 ) ... N
) )  /\  (
( ( U "
( 1 ... ( N  -  1 ) ) )  i^i  ( U " ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  (/)  /\  N  e.  ( U " (
1 ... ( N  - 
1 ) ) ) ) )  ->  (
( ( ( U
" ( 1 ... ( N  -  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( N  -  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  =  ( ( ( U " ( 1 ... ( N  - 
1 ) ) )  X.  { 1 } ) `  N ) )
319315, 317, 318mp3an12 1363 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( U "
( 1 ... ( N  -  1 ) ) )  i^i  ( U " ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  (/)  /\  N  e.  ( U " (
1 ... ( N  - 
1 ) ) ) )  ->  ( (
( ( U "
( 1 ... ( N  -  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( N  -  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N )  =  ( ( ( U
" ( 1 ... ( N  -  1 ) ) )  X. 
{ 1 } ) `
 N ) )
320280, 313, 319syl2anc 671 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
( ( U "
( 1 ... ( N  -  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( N  -  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N )  =  ( ( ( U
" ( 1 ... ( N  -  1 ) ) )  X. 
{ 1 } ) `
 N ) )
32184fvconst2 6149 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( U "
( 1 ... ( N  -  1 ) ) )  ->  (
( ( U "
( 1 ... ( N  -  1 ) ) )  X.  {
1 } ) `  N )  =  1 )
322313, 321syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
( U " (
1 ... ( N  - 
1 ) ) )  X.  { 1 } ) `  N )  =  1 )
323320, 322eqtrd 2496 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
( ( U "
( 1 ... ( N  -  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( N  -  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N )  =  1 )
324323neeq1d 2695 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
( ( ( U
" ( 1 ... ( N  -  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( N  -  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  =/=  0  <->  1  =/=  0 ) )
325271, 324mpbiri 241 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
( ( U "
( 1 ... ( N  -  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( N  -  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N )  =/=  0 )
326 df-ne 2635 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  =/=  0  <->  -.  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ...<