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

Theorem poimirlem23 31927
Description: Lemma for poimir 31937, 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 6333 . . . . . 6  |-  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
21csbex 4559 . . . . 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 2783 . . . 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 2422 . . . . 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 5880 . . . . . . 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 2697 . . . . . 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 2616 . . . . . 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 264 . . . . 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 6047 . . . 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 2870 . . 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 252 . 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 11046 . . . . . . . . . 10  |-  ( ph  ->  N  e.  ZZ )
15 poimirlem23.3 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  ( 0 ... N ) )
16 elfzelz 11807 . . . . . . . . . . 11  |-  ( V  e.  ( 0 ... N )  ->  V  e.  ZZ )
1715, 16syl 17 . . . . . . . . . 10  |-  ( ph  ->  V  e.  ZZ )
18 zlem1lt 10995 . . . . . . . . . 10  |-  ( ( N  e.  ZZ  /\  V  e.  ZZ )  ->  ( N  <_  V  <->  ( N  -  1 )  <  V ) )
1914, 17, 18syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  ( N  <_  V  <->  ( N  -  1 )  <  V ) )
20 elfzle2 11810 . . . . . . . . . . 11  |-  ( V  e.  ( 0 ... N )  ->  V  <_  N )
2115, 20syl 17 . . . . . . . . . 10  |-  ( ph  ->  V  <_  N )
2217zred 11047 . . . . . . . . . . . 12  |-  ( ph  ->  V  e.  RR )
2313nnred 10631 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  RR )
2422, 23letri3d 9784 . . . . . . . . . . 11  |-  ( ph  ->  ( V  =  N  <-> 
( V  <_  N  /\  N  <_  V ) ) )
2524biimprd 226 . . . . . . . . . 10  |-  ( ph  ->  ( ( V  <_  N  /\  N  <_  V
)  ->  V  =  N ) )
2621, 25mpand 679 . . . . . . . . 9  |-  ( ph  ->  ( N  <_  V  ->  V  =  N ) )
2719, 26sylbird 238 . . . . . . . 8  |-  ( ph  ->  ( ( N  - 
1 )  <  V  ->  V  =  N ) )
2827necon3ad 2630 . . . . . . 7  |-  ( ph  ->  ( V  =/=  N  ->  -.  ( N  - 
1 )  <  V
) )
29 nnm1nn0 10918 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
3013, 29syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
31 nn0fz0 11897 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  NN0  <->  ( N  - 
1 )  e.  ( 0 ... ( N  -  1 ) ) )
3230, 31sylib 199 . . . . . . . . . . 11  |-  ( ph  ->  ( N  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
3332adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  -> 
( N  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
34 iffalse 3920 . . . . . . . . . . . . . . . 16  |-  ( -.  ( N  -  1 )  <  V  ->  if ( ( N  - 
1 )  <  V ,  ( N  - 
1 ) ,  ( ( N  -  1 )  +  1 ) )  =  ( ( N  -  1 )  +  1 ) )
3513nncnd 10632 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  CC )
36 npcan1 10051 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
3735, 36syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
3834, 37sylan9eqr 2485 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  ->  if ( ( N  - 
1 )  <  V ,  ( N  - 
1 ) ,  ( ( N  -  1 )  +  1 ) )  =  N )
3938csbeq1d 3402 . . . . . . . . . . . . . 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 6313 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  N  ->  (
1 ... j )  =  ( 1 ... N
) )
4140imaeq2d 5187 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  N  ->  ( U " ( 1 ... j ) )  =  ( U " (
1 ... N ) ) )
4241xpeq1d 4876 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  N  ->  (
( U " (
1 ... j ) )  X.  { 1 } )  =  ( ( U " ( 1 ... N ) )  X.  { 1 } ) )
43 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  N  ->  (
j  +  1 )  =  ( N  + 
1 ) )
4443oveq1d 6320 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  N  ->  (
( j  +  1 ) ... N )  =  ( ( N  +  1 ) ... N ) )
4544imaeq2d 5187 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  N  ->  ( U " ( ( j  +  1 ) ... N ) )  =  ( U " (
( N  +  1 ) ... N ) ) )
4645xpeq1d 4876 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  N  ->  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( U " (
( N  +  1 ) ... N ) )  X.  { 0 } ) )
4742, 46uneq12d 3621 . . . . . . . . . . . . . . . . . 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 5838 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U :
( 1 ... N
) -onto-> ( 1 ... N ) )
50 foima 5815 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N )  -> 
( U " (
1 ... N ) )  =  ( 1 ... N ) )
5148, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( 1 ... N ) )
5251xpeq1d 4876 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  X.  {
1 } )  =  ( ( 1 ... N )  X.  {
1 } ) )
5323ltp1d 10544 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  N  <  ( N  +  1 ) )
5414peano2zd 11050 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
55 fzn 11822 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( N  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  <  ( N  +  1 )  <-> 
( ( N  + 
1 ) ... N
)  =  (/) ) )
5654, 14, 55syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( N  <  ( N  +  1 )  <-> 
( ( N  + 
1 ) ... N
)  =  (/) ) )
5753, 56mpbid 213 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( N  + 
1 ) ... N
)  =  (/) )
5857imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( U " (
( N  +  1 ) ... N ) )  =  ( U
" (/) ) )
5958xpeq1d 4876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( U "
( ( N  + 
1 ) ... N
) )  X.  {
0 } )  =  ( ( U " (/) )  X.  { 0 } ) )
60 ima0 5202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U
" (/) )  =  (/)
6160xpeq1i 4873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( U " (/) )  X. 
{ 0 } )  =  ( (/)  X.  {
0 } )
62 0xp 4934 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (/)  X. 
{ 0 } )  =  (/)
6361, 62eqtri 2451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( U " (/) )  X. 
{ 0 } )  =  (/)
6459, 63syl6eq 2479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( U "
( ( N  + 
1 ) ... N
) )  X.  {
0 } )  =  (/) )
6552, 64uneq12d 3621 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( U
" ( 1 ... N ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( N  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( 1 ... N
)  X.  { 1 } )  u.  (/) ) )
66 un0 3789 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1 ... N
)  X.  { 1 } )  u.  (/) )  =  ( ( 1 ... N )  X.  {
1 } )
6765, 66syl6eq 2479 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( U
" ( 1 ... N ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( N  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( 1 ... N )  X.  { 1 } ) )
6847, 67sylan9eqr 2485 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  =  N )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )  =  ( ( 1 ... N )  X. 
{ 1 } ) )
6968oveq2d 6321 . . . . . . . . . . . . . . . 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 3422 . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . 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 5883 . . . . . . . . . . . 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 11967 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0..^ K )  ->  j  e.  NN0 )
75 nn0p1nn 10916 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  NN )
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0..^ K )  ->  ( j  +  1 )  e.  NN )
77 elsni 4023 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  { 1 }  ->  y  =  1 )
7877oveq2d 6321 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  { 1 }  ->  ( j  +  y )  =  ( j  +  1 ) )
7978eleq1d 2491 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  { 1 }  ->  ( ( j  +  y )  e.  NN  <->  ( j  +  1 )  e.  NN ) )
8076, 79syl5ibrcom 225 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0..^ K )  ->  ( y  e.  { 1 }  ->  ( j  +  y )  e.  NN ) )
8180imp 430 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0..^ K )  /\  y  e.  { 1 } )  ->  ( j  +  y )  e.  NN )
8281adantl 467 . . . . . . . . . . . . . . 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 9645 . . . . . . . . . . . . . . . . 17  |-  1  e.  _V
8584fconst 5786 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... N )  X.  { 1 } ) : ( 1 ... N ) --> { 1 }
8685a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1 ... N )  X.  {
1 } ) : ( 1 ... N
) --> { 1 } )
87 ovex 6333 . . . . . . . . . . . . . . . 16  |-  ( 1 ... N )  e. 
_V
8887a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... N
)  e.  _V )
89 inidm 3671 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
9082, 83, 86, 88, 88, 89off 6560 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  oF  +  ( ( 1 ... N )  X. 
{ 1 } ) ) : ( 1 ... N ) --> NN )
91 elfz1end 11836 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  <->  N  e.  ( 1 ... N
) )
9213, 91sylib 199 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  ( 1 ... N ) )
9390, 92ffvelrnd 6038 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( T  oF  +  ( (
1 ... N )  X. 
{ 1 } ) ) `  N )  e.  NN )
9493adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( N  -  1 )  <  V )  -> 
( ( T  oF  +  ( (
1 ... N )  X. 
{ 1 } ) ) `  N )  e.  NN )
9573, 94eqeltrd 2507 . . . . . . . . . . 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 10661 . . . . . . . . . 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 4426 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( N  - 
1 )  ->  (
y  <  V  <->  ( N  -  1 )  < 
V ) )
98 id 22 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( N  - 
1 )  ->  y  =  ( N  - 
1 ) )
99 oveq1 6312 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( N  - 
1 )  ->  (
y  +  1 )  =  ( ( N  -  1 )  +  1 ) )
10097, 98, 99ifbieq12d 3938 . . . . . . . . . . . . . . 15  |-  ( y  =  ( N  - 
1 )  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  =  if ( ( N  -  1 )  <  V , 
( N  -  1 ) ,  ( ( N  -  1 )  +  1 ) ) )
101100csbeq1d 3402 . . . . . . . . . . . . . 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 5883 . . . . . . . . . . . . 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 2697 . . . . . . . . . . . 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 262 . . . . . . . . . . 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 3182 . . . . . . . . . 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 665 . . . . . . . . 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 199 . . . . . . . 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 435 . . . . . . 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 2640 . . . . 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 639 . . . 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 11045 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
113 uzid 11180 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
114 peano2uz 11219 . . . . . . . . . . . . 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 2508 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
117 fzss2 11845 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... N
) )
118116, 117syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
119118sselda 3464 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  j  e.  ( 0 ... N
) )
12092adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  N  e.  ( 1 ... N
) )
121 ffn 5746 . . . . . . . . . . . . . . 15  |-  ( T : ( 1 ... N ) --> ( 0..^ K )  ->  T  Fn  ( 1 ... N
) )
12283, 121syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  T  Fn  ( 1 ... N ) )
123122adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  T  Fn  ( 1 ... N
) )
12484fconst 5786 . . . . . . . . . . . . . . . . 17  |-  ( ( U " ( 1 ... j ) )  X.  { 1 } ) : ( U
" ( 1 ... j ) ) --> { 1 }
125 c0ex 9644 . . . . . . . . . . . . . . . . . 18  |-  0  e.  _V
126125fconst 5786 . . . . . . . . . . . . . . . . 17  |-  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( U
" ( ( j  +  1 ) ... N ) ) --> { 0 }
127124, 126pm3.2i 456 . . . . . . . . . . . . . . . 16  |-  ( ( ( U " (
1 ... j ) )  X.  { 1 } ) : ( U
" ( 1 ... j ) ) --> { 1 }  /\  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } ) : ( U " ( ( j  +  1 ) ... N ) ) --> { 0 } )
128 dff1o3 5837 . . . . . . . . . . . . . . . . . . 19  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( U :
( 1 ... N
) -onto-> ( 1 ... N )  /\  Fun  `' U ) )
129128simprbi 465 . . . . . . . . . . . . . . . . . 18  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' U
)
130 imain 5677 . . . . . . . . . . . . . . . . . 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 11807 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0 ... N )  ->  j  e.  ZZ )
133132zred 11047 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
134133ltp1d 10544 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... N )  ->  j  <  ( j  +  1 ) )
135 fzdisj 11833 . . . . . . . . . . . . . . . . . . . 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 5187 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  ( U " (/) ) )
138137, 60syl6eq 2479 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  (/) )
139131, 138sylan9req 2484 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( U " (
1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) )  =  (/) )
140 fun 5763 . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . 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 11894 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0 ... N )  ->  j  e.  NN0 )
143142, 75syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  NN )
144 nnuz 11201 . . . . . . . . . . . . . . . . . . . . 21  |-  NN  =  ( ZZ>= `  1 )
145143, 144syl6eleq 2517 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
146 elfzuz3 11804 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  j )
)
147 fzsplit2 11831 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  j )
)  ->  ( 1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
148145, 146, 147syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... N )  ->  (
1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
149148imaeq2d 5187 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... N )  ->  ( U " ( 1 ... N ) )  =  ( U " (
( 1 ... j
)  u.  ( ( j  +  1 ) ... N ) ) ) )
150 imaundi 5267 . . . . . . . . . . . . . . . . . 18  |-  ( U
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... j
) )  u.  ( U " ( ( j  +  1 ) ... N ) ) )
151149, 150syl6req 2480 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... N )  ->  (
( U " (
1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... N
) ) )  =  ( U " (
1 ... N ) ) )
152151, 51sylan9eqr 2485 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( U " (
1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... N
) ) )  =  ( 1 ... N
) )
153152feq2d 5733 . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . 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 5746 . . . . . . . . . . . . . 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 2423 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  N  e.  ( 1 ... N
) )  ->  ( T `  N )  =  ( T `  N ) )
159 eqidd 2423 . . . . . . . . . . . . 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 6554 . . . . . . . . . . . 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 672 . . . . . . . . . . 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 2424 . . . . . . . . . 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 6038 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T `  N
)  e.  ( 0..^ K ) )
164 elfzonn0 11967 . . . . . . . . . . . . . 14  |-  ( ( T `  N )  e.  ( 0..^ K )  ->  ( T `  N )  e.  NN0 )
165163, 164syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( T `  N
)  e.  NN0 )
166165nn0red 10933 . . . . . . . . . . . 12  |-  ( ph  ->  ( T `  N
)  e.  RR )
167166adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( T `  N )  e.  RR )
168165nn0ge0d 10935 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( T `  N ) )
169168adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  0  <_  ( T `  N
) )
170 1re 9649 . . . . . . . . . . . . . 14  |-  1  e.  RR
171 snssi 4144 . . . . . . . . . . . . . 14  |-  ( 1  e.  RR  ->  { 1 }  C_  RR )
172170, 171ax-mp 5 . . . . . . . . . . . . 13  |-  { 1 }  C_  RR
173 0re 9650 . . . . . . . . . . . . . 14  |-  0  e.  RR
174 snssi 4144 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  { 0 }  C_  RR )
175173, 174ax-mp 5 . . . . . . . . . . . . 13  |-  { 0 }  C_  RR
176172, 175unssi 3641 . . . . . . . . . . . 12  |-  ( { 1 }  u.  {
0 } )  C_  RR
177154, 120ffvelrnd 6038 . . . . . . . . . . . 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 3462 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  e.  RR )
179 elun 3606 . . . . . . . . . . . . 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 10144 . . . . . . . . . . . . . . 15  |-  0  <_  1
181 elsni 4023 . . . . . . . . . . . . . . 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 4460 . . . . . . . . . . . . . 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 10706 . . . . . . . . . . . . . . 15  |-  0  <_  0
184 elsni 4023 . . . . . . . . . . . . . . 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 4460 . . . . . . . . . . . . . 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 380 . . . . . . . . . . . . 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 198 . . . . . . . . . . . 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 10133 . . . . . . . . . . 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 1265 . . . . . . . . . 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 256 . . . . . . . . 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 472 . . . . . . . 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 2858 . . . . . . 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 466 . . . . . 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 4427 . . . . . . . . . . . . . 14  |-  ( V  =  N  ->  (
y  <  V  <->  y  <  N ) )
196195ifbid 3933 . . . . . . . . . . . . 13  |-  ( V  =  N  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  =  if ( y  <  N , 
y ,  ( y  +  1 ) ) )
197 elfzelz 11807 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  ZZ )
198197zred 11047 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  RR )
199198adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  e.  RR )
20030nn0red 10933 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  e.  RR )
201200adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
20223adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  RR )
203 elfzle2 11810 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  <_  ( N  -  1 ) )
204203adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <_  ( N  -  1 ) )
20523ltm1d 10546 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  <  N )
206205adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
207199, 201, 202, 204, 206lelttrd 9800 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <  N )
208207iftrued 3919 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  if ( y  <  N ,  y ,  ( y  +  1 ) )  =  y )
209196, 208sylan9eqr 2485 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  V  =  N )  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  =  y )
210209an32s 811 . . . . . . . . . . 11  |-  ( ( ( ph  /\  V  =  N )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  if ( y  <  V ,  y ,  ( y  +  1 ) )  =  y )
211210csbeq1d 3402 . . . . . . . . . 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 5883 . . . . . . . . 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 2424 . . . . . . . 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 2858 . . . . . . 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 1755 . . . . . . . 8  |-  F/ y ( ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0
216 nfcsb1v 3411 . . . . . . . . . 10  |-  F/_ j [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )
217 nfcv 2580 . . . . . . . . . 10  |-  F/_ j N
218216, 217nffv 5888 . . . . . . . . 9  |-  F/_ j
( [_ y  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )
219218nfeq1 2595 . . . . . . . 8  |-  F/ j ( [_ y  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  N )  =  0
220 csbeq1a 3404 . . . . . . . . . 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 5883 . . . . . . . . 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 2424 . . . . . . . 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 3050 . . . . . . 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 266 . . . . . 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 3767 . . . . . . . . . 10  |-  ( ( N  -  1 )  e.  ( 0 ... ( N  -  1 ) )  ->  (
0 ... ( N  - 
1 ) )  =/=  (/) )
226 r19.3rzv 3892 . . . . . . . . . 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 11807 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  j  e.  ZZ )
229228zred 11047 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  j  e.  RR )
230229ltp1d 10544 . . . . . . . . . . . . . . . . . . 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 5187 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  ( U " (/) ) )
233232, 60syl6eq 2479 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  (/) )
234131, 233sylan9req 2484 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( U " (
1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) )  =  (/) )
235234adantlr 719 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( U " (
1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... N
) ) )  =  (/) )
236 simplr 760 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( U `  N )  =  N )
237 f1ofn 5832 . . . . . . . . . . . . . . . . . . 19  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U  Fn  ( 1 ... N
) )
23848, 237syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U  Fn  ( 1 ... N ) )
239238adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  U  Fn  ( 1 ... N
) )
240 elfznn0 11894 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  j  e.  NN0 )
241240, 75syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  (
j  +  1 )  e.  NN )
242241, 144syl6eleq 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
243 fzss1 11844 . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( j  +  1 ) ... N ) 
C_  ( 1 ... N ) )
24637adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  =  N )
247 elfzuz3 11804 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  ( ZZ>= `  j
) )
248 eluzp1p1 11191 . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  (
j  +  1 ) ) )
251246, 250eqeltrrd 2508 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  ( j  +  1 ) ) )
252 eluzfz2 11814 . . . . . . . . . . . . . . . . . 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 6158 . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( U `  N )  e.  ( U " (
( j  +  1 ) ... N ) ) )
256255adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( U `  N )  e.  ( U " (
( j  +  1 ) ... N ) ) )
257236, 256eqeltrrd 2508 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( U `  N )  =  N )  /\  j  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( U " (
( j  +  1 ) ... N ) ) )
258 fnconstg 5788 . . . . . . . . . . . . . . . 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 5788 . . . . . . . . . . . . . . . 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 5953 . . . . . . . . . . . . . . 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 1350 . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . 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 6135 . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . 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 2836 . . . . . . . . . . 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 435 . . . . . . . . . 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 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( N  -  1 )  e.  ( 0 ... ( N  -  1 ) ) )
271 ax-1ne0 9615 . . . . . . . . . . . . . . 15  |-  1  =/=  0
272 imain 5677 . . . . . . . . . . . . . . . . . . . . 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 4450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( N  -  1 )  <  ( ( N  -  1 )  +  1 ) )
275 fzdisj 11833 . . . . . . . . . . . . . . . . . . . . . . 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 5187 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... ( N  -  1 ) )  i^i  ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  ( U
" (/) ) )
278277, 60syl6eq 2479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... ( N  -  1 ) )  i^i  ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  (/) )
279273, 278eqtr3d 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... ( N  -  1 ) ) )  i^i  ( U " ( ( ( N  -  1 )  +  1 ) ... N ) ) )  =  (/) )
280279adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( ( U " ( 1 ... ( N  -  1 ) ) )  i^i  ( U " (
( ( N  - 
1 )  +  1 ) ... N ) ) )  =  (/) )
28192adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  N  e.  ( 1 ... N
) )
282 elimasni 5214 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( U " { N } )  ->  N U N )
283 fnbrfvb 5921 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( U  Fn  ( 1 ... N )  /\  N  e.  ( 1 ... N ) )  ->  ( ( U `
 N )  =  N  <->  N U N ) )
284238, 92, 283syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( U `  N )  =  N  <-> 
N U N ) )
285282, 284syl5ibr 224 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( N  e.  ( U " { N } )  ->  ( U `  N )  =  N ) )
286285necon3ad 2630 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( U `  N )  =/=  N  ->  -.  N  e.  ( U " { N } ) ) )
287286imp 430 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  -.  N  e.  ( U " { N } ) )
288281, 287eldifd 3447 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  N  e.  ( ( 1 ... N )  \  ( U " { N }
) ) )
289 imadif 5676 . . . . . . . . . . . . . . . . . . . . . 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 3877 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... ( N  -  1 ) )  u.  { N } )  \  { N } )  =  ( ( 1 ... ( N  -  1 ) )  \  { N } )
29213, 144syl6eleq 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
293 fzm1 11881 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( ( 1 ... ( N  - 
1 ) )  u. 
{ N } )  <-> 
( j  e.  ( 1 ... ( N  -  1 ) )  \/  j  e.  { N } ) )
296 elsn 4012 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  { N }  <->  j  =  N )
297296orbi2i 521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  ( 1 ... ( N  - 
1 ) )  \/  j  e.  { N } )  <->  ( j  e.  ( 1 ... ( N  -  1 ) )  \/  j  =  N ) )
298295, 297bitri 252 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  e.  ( ( 1 ... ( N  - 
1 ) )  u. 
{ N } )  <-> 
( j  e.  ( 1 ... ( N  -  1 ) )  \/  j  =  N ) )
299294, 298syl6rbbr 267 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( j  e.  ( ( 1 ... ( N  -  1 ) )  u.  { N } )  <->  j  e.  ( 1 ... N
) ) )
300299eqrdv 2419 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( 1 ... ( N  -  1 ) )  u.  { N } )  =  ( 1 ... N ) )
301300difeq1d 3582 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( 1 ... ( N  - 
1 ) )  u. 
{ N } ) 
\  { N }
)  =  ( ( 1 ... N ) 
\  { N }
) )
302200, 23ltnled 9789 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( N  - 
1 )  <  N  <->  -.  N  <_  ( N  -  1 ) ) )
303205, 302mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  -.  N  <_  ( N  -  1 ) )
304 elfzle2 11810 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  <_  ( N  -  1 ) )
305303, 304nsyl 124 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  -.  N  e.  ( 1 ... ( N  -  1 ) ) )
306 difsn 4134 . . . . . . . . . . . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1 ... N )  \  { N } )  =  ( 1 ... ( N  -  1 ) ) )
309308imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { N } ) )  =  ( U " (
1 ... ( N  - 
1 ) ) ) )
31051difeq1d 3582 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { N }
) )  =  ( ( 1 ... N
)  \  ( U " { N } ) ) )
311290, 309, 3103eqtr3rd 2472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( 1 ... N )  \  ( U " { N }
) )  =  ( U " ( 1 ... ( N  - 
1 ) ) ) )
312311adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
1 ... N )  \ 
( U " { N } ) )  =  ( U " (
1 ... ( N  - 
1 ) ) ) )
313288, 312eleqtrd 2509 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  N  e.  ( U " ( 1 ... ( N  - 
1 ) ) ) )
314 fnconstg 5788 . . . . . . . . . . . . . . . . . . . 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 5788 . . . . . . . . . . . . . . . . . . . 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 5952 . . . . . . . . . . . . . . . . . . 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 1350 . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . 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 6135 . . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
( ( U "
( 1 ... ( N  -  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( N  -  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N )  =  1 )
324323neeq1d 2697 . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( U `  N )  =/=  N
)  ->  ( (
( ( U "
( 1 ... ( N  -  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( N  -  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 N )  =/=  0 )
326 df-ne 2616 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  N )  =/=  0  <->  -.  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... N )