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

Theorem poimirlem31 31891
Description: Lemma for poimir 31893, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 31890 and poimirlem28 31888. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimir.i  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
poimir.r  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
poimir.1  |-  ( ph  ->  F  e.  ( ( Rt  I )  Cn  R
) )
poimir.2  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  z  e.  I  /\  ( z `  n )  =  0 ) )  ->  (
( F `  z
) `  n )  <_  0 )
poimirlem31.p  |-  P  =  ( ( 1st `  ( G `  k )
)  oF  +  ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )
poimirlem31.3  |-  ( ph  ->  G : NN --> ( ( NN0  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
poimirlem31.4  |-  ( (
ph  /\  k  e.  NN )  ->  ran  ( 1st `  ( G `  k ) )  C_  ( 0..^ k ) )
poimirlem31.5  |-  ( (
ph  /\  ( k  e.  NN  /\  i  e.  ( 0 ... N
) ) )  ->  E. j  e.  (
0 ... N ) i  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )
Assertion
Ref Expression
poimirlem31  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 1 ... N
)  /\  r  e.  {  <_  ,  `'  <_  } ) )  ->  E. j  e.  ( 0 ... N
) 0 r ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) )
Distinct variable groups:    f, i,
j, k, n, z    ph, j, n    j, F, n    j, N, n    ph, i, k    f, N, i, k    ph, z    f, F, k, z    z, N    i, r, j, k, n, z, ph    a, b, f, i, j, k, n, r, z, F    G, a, b, f, i, j, k, n, r, z    I, a, b, f, i, j, k, n, r, z    N, a, b, r    R, a, b, f, i, j, k, n, r, z    P, a, b, f, i, n, r, z
Allowed substitution hints:    ph( f, a, b)    P( j, k)

Proof of Theorem poimirlem31
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elpri 4014 . . . 4  |-  ( r  e.  {  <_  ,  `'  <_  }  ->  ( r  =  <_  \/  r  =  `'  <_  ) )
2 simprr 765 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 1 ... N
) ) )  ->  n  e.  ( 1 ... N ) )
3 1eluzge0 11204 . . . . . . . . . . 11  |-  1  e.  ( ZZ>= `  0 )
4 fzss1 11839 . . . . . . . . . . 11  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
53, 4ax-mp 5 . . . . . . . . . 10  |-  ( 1 ... N )  C_  ( 0 ... N
)
65sseli 3461 . . . . . . . . 9  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ( 0 ... N
) )
76anim2i 572 . . . . . . . 8  |-  ( ( k  e.  NN  /\  n  e.  ( 1 ... N ) )  ->  ( k  e.  NN  /\  n  e.  ( 0 ... N
) ) )
8 eleq1 2495 . . . . . . . . . . . . 13  |-  ( i  =  n  ->  (
i  e.  ( 0 ... N )  <->  n  e.  ( 0 ... N
) ) )
98anbi2d 709 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
( k  e.  NN  /\  i  e.  ( 0 ... N ) )  <-> 
( k  e.  NN  /\  n  e.  ( 0 ... N ) ) ) )
109anbi2d 709 . . . . . . . . . . 11  |-  ( i  =  n  ->  (
( ph  /\  (
k  e.  NN  /\  i  e.  ( 0 ... N ) ) )  <->  ( ph  /\  ( k  e.  NN  /\  n  e.  ( 0 ... N ) ) ) ) )
11 eqeq1 2427 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
i  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  <->  n  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) ) )
1211rexbidv 2940 . . . . . . . . . . 11  |-  ( i  =  n  ->  ( E. j  e.  (
0 ... N ) i  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  <->  E. j  e.  ( 0 ... N ) n  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )
) )
1310, 12imbi12d 322 . . . . . . . . . 10  |-  ( i  =  n  ->  (
( ( ph  /\  ( k  e.  NN  /\  i  e.  ( 0 ... N ) ) )  ->  E. j  e.  ( 0 ... N
) i  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )  <->  ( ( ph  /\  ( k  e.  NN  /\  n  e.  ( 0 ... N
) ) )  ->  E. j  e.  (
0 ... N ) n  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) ) ) )
14 poimirlem31.5 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  i  e.  ( 0 ... N
) ) )  ->  E. j  e.  (
0 ... N ) i  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )
1513, 14chvarv 2069 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 0 ... N
) ) )  ->  E. j  e.  (
0 ... N ) n  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )
16 elfzle1 11804 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... N )  ->  1  <_  n )
17 1re 9644 . . . . . . . . . . . . . 14  |-  1  e.  RR
18 elfzelz 11802 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ZZ )
1918zred 11042 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  n  e.  RR )
20 lenlt 9714 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  RR  /\  n  e.  RR )  ->  ( 1  <_  n  <->  -.  n  <  1 ) )
2117, 19, 20sylancr 668 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... N )  ->  (
1  <_  n  <->  -.  n  <  1 ) )
2216, 21mpbid 214 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... N )  ->  -.  n  <  1 )
23 elsni 4022 . . . . . . . . . . . . 13  |-  ( n  e.  { 0 }  ->  n  =  0 )
24 0lt1 10138 . . . . . . . . . . . . 13  |-  0  <  1
2523, 24syl6eqbr 4459 . . . . . . . . . . . 12  |-  ( n  e.  { 0 }  ->  n  <  1
)
2622, 25nsyl 125 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... N )  ->  -.  n  e.  { 0 } )
27 ltso 9716 . . . . . . . . . . . . . . 15  |-  <  Or  RR
28 snfi 7655 . . . . . . . . . . . . . . . . 17  |-  { 0 }  e.  Fin
29 fzfi 12186 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... N )  e. 
Fin
30 rabfi 7800 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1 ... N )  e.  Fin  ->  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) }  e.  Fin )
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) }  e.  Fin
32 unfi 7842 . . . . . . . . . . . . . . . . 17  |-  ( ( { 0 }  e.  Fin  /\  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) }  e.  Fin )  ->  ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  e.  Fin )
3328, 31, 32mp2an 677 . . . . . . . . . . . . . . . 16  |-  ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  e.  Fin
34 c0ex 9639 . . . . . . . . . . . . . . . . . 18  |-  0  e.  _V
3534snid 4025 . . . . . . . . . . . . . . . . 17  |-  0  e.  { 0 }
36 elun1 3634 . . . . . . . . . . . . . . . . 17  |-  ( 0  e.  { 0 }  ->  0  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) )
37 ne0i 3768 . . . . . . . . . . . . . . . . 17  |-  ( 0  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  ->  ( {
0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  =/=  (/) )
3835, 36, 37mp2b 10 . . . . . . . . . . . . . . . 16  |-  ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  =/=  (/)
39 0re 9645 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
40 snssi 4142 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  { 0 }  C_  RR )
4139, 40ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  { 0 }  C_  RR
42 ssrab2 3547 . . . . . . . . . . . . . . . . . 18  |-  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } 
C_  ( 1 ... N )
4318ssriv 3469 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ... N )  C_  ZZ
44 zssre 10946 . . . . . . . . . . . . . . . . . . 19  |-  ZZ  C_  RR
4543, 44sstri 3474 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... N )  C_  RR
4642, 45sstri 3474 . . . . . . . . . . . . . . . . 17  |-  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } 
C_  RR
4741, 46unssi 3642 . . . . . . . . . . . . . . . 16  |-  ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  C_  RR
4833, 38, 473pm3.2i 1184 . . . . . . . . . . . . . . 15  |-  ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  e.  Fin  /\  ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  =/=  (/)  /\  ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  C_  RR )
49 fisupcl 7989 . . . . . . . . . . . . . . 15  |-  ( (  <  Or  RR  /\  ( ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  e.  Fin  /\  ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  =/=  (/)  /\  ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  C_  RR )
)  ->  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) )
5027, 48, 49mp2an 677 . . . . . . . . . . . . . 14  |-  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } )
51 eleq1 2495 . . . . . . . . . . . . . 14  |-  ( n  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( n  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } )  <->  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ) )
5250, 51mpbiri 237 . . . . . . . . . . . . 13  |-  ( n  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  n  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) )
53 elun 3607 . . . . . . . . . . . . 13  |-  ( n  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  <->  ( n  e. 
{ 0 }  \/  n  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) )
5452, 53sylib 200 . . . . . . . . . . . 12  |-  ( n  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( n  e.  { 0 }  \/  n  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) )
55 oveq2 6311 . . . . . . . . . . . . . . . 16  |-  ( a  =  n  ->  (
1 ... a )  =  ( 1 ... n
) )
5655raleqdv 3032 . . . . . . . . . . . . . . 15  |-  ( a  =  n  ->  ( A. b  e.  (
1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  <->  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
5756elrab 3230 . . . . . . . . . . . . . 14  |-  ( n  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) }  <->  ( n  e.  ( 1 ... N
)  /\  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
58 elfzuz 11798 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ( ZZ>= `  1 )
)
59 eluzfz2 11809 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( ZZ>= `  1
)  ->  n  e.  ( 1 ... n
) )
6058, 59syl 17 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ( 1 ... n
) )
61 simpl 459 . . . . . . . . . . . . . . . 16  |-  ( ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  -> 
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b ) )
6261ralimi 2819 . . . . . . . . . . . . . . 15  |-  ( A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  ->  A. b  e.  (
1 ... n ) 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  b
) )
63 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( b  =  n  ->  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  =  ( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
) )
6463breq2d 4433 . . . . . . . . . . . . . . . 16  |-  ( b  =  n  ->  (
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  <->  0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) ) )
6564rspcva 3181 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  ( 1 ... n )  /\  A. b  e.  ( 1 ... n ) 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  b
) )  ->  0  <_  ( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
) )
6660, 62, 65syl2an 480 . . . . . . . . . . . . . 14  |-  ( ( n  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) )
6757, 66sylbi 199 . . . . . . . . . . . . 13  |-  ( n  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) }  ->  0  <_  ( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
) )
6867orim2i 521 . . . . . . . . . . . 12  |-  ( ( n  e.  { 0 }  \/  n  e. 
{ a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } )  -> 
( n  e.  {
0 }  \/  0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
) ) )
6954, 68syl 17 . . . . . . . . . . 11  |-  ( n  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( n  e.  { 0 }  \/  0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
) ) )
70 orel1 384 . . . . . . . . . . 11  |-  ( -.  n  e.  { 0 }  ->  ( (
n  e.  { 0 }  \/  0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
) )  ->  0  <_  ( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
) ) )
7126, 69, 70syl2im 40 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... N )  ->  (
n  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) ) )
7271reximdv 2900 . . . . . . . . 9  |-  ( n  e.  ( 1 ... N )  ->  ( E. j  e.  (
0 ... N ) n  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  E. j  e.  ( 0 ... N
) 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) ) )
7315, 72syl5 34 . . . . . . . 8  |-  ( n  e.  ( 1 ... N )  ->  (
( ph  /\  (
k  e.  NN  /\  n  e.  ( 0 ... N ) ) )  ->  E. j  e.  ( 0 ... N
) 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) ) )
747, 73sylan2i 660 . . . . . . 7  |-  ( n  e.  ( 1 ... N )  ->  (
( ph  /\  (
k  e.  NN  /\  n  e.  ( 1 ... N ) ) )  ->  E. j  e.  ( 0 ... N
) 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) ) )
752, 74mpcom 38 . . . . . 6  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 1 ... N
) ) )  ->  E. j  e.  (
0 ... N ) 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
) )
76 breq 4423 . . . . . . 7  |-  ( r  =  <_  ->  ( 0 r ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
)  <->  0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) ) )
7776rexbidv 2940 . . . . . 6  |-  ( r  =  <_  ->  ( E. j  e.  ( 0 ... N ) 0 r ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
)  <->  E. j  e.  ( 0 ... N ) 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) ) )
7875, 77syl5ibrcom 226 . . . . 5  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 1 ... N
) ) )  -> 
( r  =  <_  ->  E. j  e.  ( 0 ... N ) 0 r ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) ) )
79 poimir.0 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  NN )
8079nnzd 11041 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  ZZ )
81 elfzm1b 11874 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  ZZ  /\  N  e.  ZZ )  ->  ( n  e.  ( 1 ... N )  <-> 
( n  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) ) )
8218, 80, 81syl2anr 481 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
n  e.  ( 1 ... N )  <->  ( n  -  1 )  e.  ( 0 ... ( N  -  1 ) ) ) )
8382biimpd 211 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
n  e.  ( 1 ... N )  -> 
( n  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) ) )
8483ex 436 . . . . . . . . . . . 12  |-  ( ph  ->  ( n  e.  ( 1 ... N )  ->  ( n  e.  ( 1 ... N
)  ->  ( n  -  1 )  e.  ( 0 ... ( N  -  1 ) ) ) ) )
8584pm2.43d 51 . . . . . . . . . . 11  |-  ( ph  ->  ( n  e.  ( 1 ... N )  ->  ( n  - 
1 )  e.  ( 0 ... ( N  -  1 ) ) ) )
8679nncnd 10627 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  CC )
87 npcan1 10046 . . . . . . . . . . . . . . 15  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
8886, 87syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
89 nnm1nn0 10913 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
9079, 89syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
9190nn0zd 11040 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
92 uzid 11175 . . . . . . . . . . . . . . 15  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
93 peano2uz 11214 . . . . . . . . . . . . . . 15  |-  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
9491, 92, 933syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
9588, 94eqeltrrd 2512 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
96 fzss2 11840 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... N
) )
9795, 96syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
9897sseld 3464 . . . . . . . . . . 11  |-  ( ph  ->  ( ( n  - 
1 )  e.  ( 0 ... ( N  -  1 ) )  ->  ( n  - 
1 )  e.  ( 0 ... N ) ) )
9985, 98syld 46 . . . . . . . . . 10  |-  ( ph  ->  ( n  e.  ( 1 ... N )  ->  ( n  - 
1 )  e.  ( 0 ... N ) ) )
10099anim2d 568 . . . . . . . . 9  |-  ( ph  ->  ( ( k  e.  NN  /\  n  e.  ( 1 ... N
) )  ->  (
k  e.  NN  /\  ( n  -  1
)  e.  ( 0 ... N ) ) ) )
101100imp 431 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 1 ... N
) ) )  -> 
( k  e.  NN  /\  ( n  -  1 )  e.  ( 0 ... N ) ) )
102 ovex 6331 . . . . . . . . 9  |-  ( n  -  1 )  e. 
_V
103 eleq1 2495 . . . . . . . . . . . 12  |-  ( i  =  ( n  - 
1 )  ->  (
i  e.  ( 0 ... N )  <->  ( n  -  1 )  e.  ( 0 ... N
) ) )
104103anbi2d 709 . . . . . . . . . . 11  |-  ( i  =  ( n  - 
1 )  ->  (
( k  e.  NN  /\  i  e.  ( 0 ... N ) )  <-> 
( k  e.  NN  /\  ( n  -  1 )  e.  ( 0 ... N ) ) ) )
105104anbi2d 709 . . . . . . . . . 10  |-  ( i  =  ( n  - 
1 )  ->  (
( ph  /\  (
k  e.  NN  /\  i  e.  ( 0 ... N ) ) )  <->  ( ph  /\  ( k  e.  NN  /\  ( n  -  1 )  e.  ( 0 ... N ) ) ) ) )
106 eqeq1 2427 . . . . . . . . . . 11  |-  ( i  =  ( n  - 
1 )  ->  (
i  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  <->  ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) ) )
107106rexbidv 2940 . . . . . . . . . 10  |-  ( i  =  ( n  - 
1 )  ->  ( E. j  e.  (
0 ... N ) i  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  <->  E. j  e.  ( 0 ... N ) ( n  -  1 )  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )
) )
108105, 107imbi12d 322 . . . . . . . . 9  |-  ( i  =  ( n  - 
1 )  ->  (
( ( ph  /\  ( k  e.  NN  /\  i  e.  ( 0 ... N ) ) )  ->  E. j  e.  ( 0 ... N
) i  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )  <->  ( ( ph  /\  ( k  e.  NN  /\  ( n  -  1 )  e.  ( 0 ... N
) ) )  ->  E. j  e.  (
0 ... N ) ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) ) ) )
109102, 108, 14vtocl 3134 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  NN  /\  ( n  -  1 )  e.  ( 0 ... N
) ) )  ->  E. j  e.  (
0 ... N ) ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )
110101, 109syldan 473 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 1 ... N
) ) )  ->  E. j  e.  (
0 ... N ) ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )
111 eleq1 2495 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( (
n  -  1 )  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  <->  sup ( ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  e.  ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ) )
11250, 111mpbiri 237 . . . . . . . . . . . . . . 15  |-  ( ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( n  -  1 )  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) )
113 elun 3607 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  <->  ( ( n  -  1 )  e. 
{ 0 }  \/  ( n  -  1
)  e.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) )
114102elsnc 4021 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  { 0 }  <-> 
( n  -  1 )  =  0 )
115 oveq2 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( n  - 
1 )  ->  (
1 ... a )  =  ( 1 ... (
n  -  1 ) ) )
116115raleqdv 3032 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( n  - 
1 )  ->  ( A. b  e.  (
1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  <->  A. b  e.  ( 1 ... (
n  -  1 ) ) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
117116elrab 3230 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) }  <->  ( (
n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
118114, 117orbi12i 524 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  -  1 )  e.  { 0 }  \/  ( n  -  1 )  e. 
{ a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } )  <->  ( (
n  -  1 )  =  0  \/  (
( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) ) )
119113, 118bitri 253 . . . . . . . . . . . . . . 15  |-  ( ( n  -  1 )  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  <->  ( ( n  -  1 )  =  0  \/  ( ( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) ) )
120112, 119sylib 200 . . . . . . . . . . . . . 14  |-  ( ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( (
n  -  1 )  =  0  \/  (
( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) ) )
121120a1i 11 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  ( ( n  - 
1 )  =  0  \/  ( ( n  -  1 )  e.  ( 1 ... N
)  /\  A. b  e.  ( 1 ... (
n  -  1 ) ) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) ) ) )
122 ltm1 10447 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  RR  ->  (
n  -  1 )  <  n )
123 peano2rem 9943 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR  ->  (
n  -  1 )  e.  RR )
124 ltnle 9715 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  -  1 )  e.  RR  /\  n  e.  RR )  ->  ( ( n  - 
1 )  <  n  <->  -.  n  <_  ( n  -  1 ) ) )
125123, 124mpancom 674 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  RR  ->  (
( n  -  1 )  <  n  <->  -.  n  <_  ( n  -  1 ) ) )
126122, 125mpbid 214 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  -.  n  <_  ( n  - 
1 ) )
12719, 126syl 17 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... N )  ->  -.  n  <_  ( n  - 
1 ) )
128 breq2 4425 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( n  <_  ( n  -  1 )  <->  n  <_  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )
) )
129128notbid 296 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( -.  n  <_  ( n  - 
1 )  <->  -.  n  <_  sup ( ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) ) )
130127, 129syl5ibcom 224 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  -.  n  <_  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) ) )
131 elun2 3635 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) }  ->  n  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) )
132 fimaxre2 10554 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } )  C_  RR  /\  ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  e.  Fin )  ->  E. x  e.  RR  A. y  e.  ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) y  <_  x
)
13347, 33, 132mp2an 677 . . . . . . . . . . . . . . . . . . . 20  |-  E. x  e.  RR  A. y  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) y  <_  x
13447, 38, 1333pm3.2i 1184 . . . . . . . . . . . . . . . . . . 19  |-  ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  C_  RR  /\  ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  =/=  (/)  /\  E. x  e.  RR  A. y  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) y  <_  x )
135134suprubii 10584 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )  ->  n  <_  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )
136131, 135syl 17 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) }  ->  n  <_  sup ( ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  ) )
137136con3i 141 . . . . . . . . . . . . . . . 16  |-  ( -.  n  <_  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  -.  n  e.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } )
138 ianor 491 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( n  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) )  <->  ( -.  n  e.  ( 1 ... N )  \/ 
-.  A. b  e.  ( 1 ... n ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
139138, 57xchnxbir 311 . . . . . . . . . . . . . . . 16  |-  ( -.  n  e.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) }  <-> 
( -.  n  e.  ( 1 ... N
)  \/  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
140137, 139sylib 200 . . . . . . . . . . . . . . 15  |-  ( -.  n  <_  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  ( -.  n  e.  ( 1 ... N
)  \/  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
141130, 140syl6 35 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  ( -.  n  e.  ( 1 ... N
)  \/  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) ) )
142 pm2.63 796 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  ( 1 ... N )  \/ 
-.  A. b  e.  ( 1 ... n ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  ( ( -.  n  e.  ( 1 ... N )  \/ 
-.  A. b  e.  ( 1 ... n ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  -.  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
143142orcs 396 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  (
( -.  n  e.  ( 1 ... N
)  \/  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  -.  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
144141, 143syld 46 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  -.  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
145121, 144jcad 536 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  ( ( ( n  -  1 )  =  0  \/  ( ( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )  /\  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) ) )
146 andir 877 . . . . . . . . . . . . . 14  |-  ( ( ( ( n  - 
1 )  =  0  \/  ( ( n  -  1 )  e.  ( 1 ... N
)  /\  A. b  e.  ( 1 ... (
n  -  1 ) ) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )  /\  -.  A. b  e.  ( 1 ... n ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  <-> 
( ( ( n  -  1 )  =  0  /\  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  \/  ( ( ( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  /\  -.  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) ) )
147 1p0e1 10724 . . . . . . . . . . . . . . . . . 18  |-  ( 1  +  0 )  =  1
14818zcnd 11043 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  n  e.  CC )
149 ax-1cn 9599 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
150 0cn 9637 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  CC
151 subadd 9880 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  CC  /\  1  e.  CC  /\  0  e.  CC )  ->  (
( n  -  1 )  =  0  <->  (
1  +  0 )  =  n ) )
152149, 150, 151mp3an23 1353 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  CC  ->  (
( n  -  1 )  =  0  <->  (
1  +  0 )  =  n ) )
153148, 152syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  0  <->  (
1  +  0 )  =  n ) )
154153biimpa 487 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  ( 1 ... N )  /\  ( n  -  1
)  =  0 )  ->  ( 1  +  0 )  =  n )
155147, 154syl5reqr 2479 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  ( 1 ... N )  /\  ( n  -  1
)  =  0 )  ->  n  =  1 )
156 1z 10969 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  ZZ
157 fzsn 11842 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
158156, 157ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1 ... 1 )  =  { 1 }
159 oveq2 6311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  1  ->  (
1 ... n )  =  ( 1 ... 1
) )
160 sneq 4007 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  1  ->  { n }  =  { 1 } )
161158, 159, 1603eqtr4a 2490 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
1 ... n )  =  { n } )
162161raleqdv 3032 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  ( A. b  e.  (
1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  <->  A. b  e.  { n }  (
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
163162notbid 296 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  ( -.  A. b  e.  ( 1 ... n ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  <->  -.  A. b  e.  { n }  (
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
164163biimpd 211 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( -.  A. b  e.  ( 1 ... n ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  ->  -.  A. b  e.  {
n }  ( 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
165155, 164syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  ( 1 ... N )  /\  ( n  -  1
)  =  0 )  ->  ( -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  ->  -.  A. b  e.  {
n }  ( 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
166165expimpd 607 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... N )  ->  (
( ( n  - 
1 )  =  0  /\  -.  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) )  ->  -.  A. b  e.  { n }  ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
167 ralun 3649 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. b  e.  ( 1 ... ( n  -  1 ) ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  /\  A. b  e.  { n }  ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) )  ->  A. b  e.  ( ( 1 ... ( n  -  1 ) )  u.  {
n } ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )
168 npcan1 10046 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  CC  ->  (
( n  -  1 )  +  1 )  =  n )
169148, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  +  1 )  =  n )
170169, 58eqeltrd 2511 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  +  1 )  e.  ( ZZ>= `  1
) )
171 peano2zm 10982 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  ZZ  ->  (
n  -  1 )  e.  ZZ )
172 uzid 11175 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  -  1 )  e.  ZZ  ->  (
n  -  1 )  e.  ( ZZ>= `  (
n  -  1 ) ) )
173 peano2uz 11214 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  -  1 )  e.  ( ZZ>= `  (
n  -  1 ) )  ->  ( (
n  -  1 )  +  1 )  e.  ( ZZ>= `  ( n  -  1 ) ) )
17418, 171, 172, 1734syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  +  1 )  e.  ( ZZ>= `  (
n  -  1 ) ) )
175169, 174eqeltrrd 2512 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ( ZZ>= `  ( n  -  1 ) ) )
176 fzsplit2 11826 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( n  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  n  e.  ( ZZ>= `  ( n  -  1 ) ) )  ->  ( 1 ... n )  =  ( ( 1 ... ( n  -  1 ) )  u.  (
( ( n  - 
1 )  +  1 ) ... n ) ) )
177170, 175, 176syl2anc 666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( 1 ... N )  ->  (
1 ... n )  =  ( ( 1 ... ( n  -  1 ) )  u.  (
( ( n  - 
1 )  +  1 ) ... n ) ) )
178169oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
( ( n  - 
1 )  +  1 ) ... n )  =  ( n ... n ) )
179 fzsn 11842 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  ZZ  ->  (
n ... n )  =  { n } )
18018, 179syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
n ... n )  =  { n } )
181178, 180eqtrd 2464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  (
( ( n  - 
1 )  +  1 ) ... n )  =  { n }
)
182181uneq2d 3621 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( 1 ... N )  ->  (
( 1 ... (
n  -  1 ) )  u.  ( ( ( n  -  1 )  +  1 ) ... n ) )  =  ( ( 1 ... ( n  - 
1 ) )  u. 
{ n } ) )
183177, 182eqtrd 2464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... N )  ->  (
1 ... n )  =  ( ( 1 ... ( n  -  1 ) )  u.  {
n } ) )
184183raleqdv 3032 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  ( A. b  e.  (
1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  <->  A. b  e.  ( ( 1 ... ( n  -  1 ) )  u.  {
n } ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
185167, 184syl5ibr 225 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  (
( A. b  e.  ( 1 ... (
n  -  1 ) ) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
)  /\  A. b  e.  { n }  (
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  A. b  e.  ( 1 ... n ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
186185expdimp 439 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  ( A. b  e.  { n }  (
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  ->  A. b  e.  (
1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
187186con3d 139 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  ( -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  ->  -.  A. b  e.  {
n }  ( 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
188187adantrl 721 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  ( 1 ... N )  /\  ( ( n  - 
1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... (
n  -  1 ) ) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )  -> 
( -.  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
)  ->  -.  A. b  e.  { n }  (
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
189188expimpd 607 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... N )  ->  (
( ( ( n  -  1 )  e.  ( 1 ... N
)  /\  A. b  e.  ( 1 ... (
n  -  1 ) ) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) )  /\  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  -.  A. b  e.  { n }  (
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
190166, 189jaod 382 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  (
( ( ( n  -  1 )  =  0  /\  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  \/  ( ( ( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  /\  -.  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )  ->  -.  A. b  e.  {
n }  ( 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) ) )
191146, 190syl5bi 221 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... N )  ->  (
( ( ( n  -  1 )  =  0  \/  ( ( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )  /\  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  -.  A. b  e.  { n }  (
0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )
192 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  n  ->  ( P `  b )  =  ( P `  n ) )
193192neeq1d 2702 . . . . . . . . . . . . . . . . 17  |-  ( b  =  n  ->  (
( P `  b
)  =/=  0  <->  ( P `  n )  =/=  0 ) )
19464, 193anbi12d 716 . . . . . . . . . . . . . . . 16  |-  ( b  =  n  ->  (
( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 )  <->  ( 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
)  /\  ( P `  n )  =/=  0
) ) )
195194ralsng 4032 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... N )  ->  ( A. b  e.  { n }  ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
)  <->  ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
)  /\  ( P `  n )  =/=  0
) ) )
196195notbid 296 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  ( -.  A. b  e.  {
n }  ( 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
)  <->  -.  ( 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
)  /\  ( P `  n )  =/=  0
) ) )
197 ianor 491 . . . . . . . . . . . . . . 15  |-  ( -.  ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n )  /\  ( P `  n )  =/=  0 )  <->  ( -.  0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
)  \/  -.  ( P `  n )  =/=  0 ) )
198 nne 2625 . . . . . . . . . . . . . . . 16  |-  ( -.  ( P `  n
)  =/=  0  <->  ( P `  n )  =  0 )
199198orbi2i 522 . . . . . . . . . . . . . . 15  |-  ( ( -.  0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n )  \/ 
-.  ( P `  n )  =/=  0
)  <->  ( -.  0  <_  ( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
)  \/  ( P `
 n )  =  0 ) )
200197, 199bitri 253 . . . . . . . . . . . . . 14  |-  ( -.  ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n )  /\  ( P `  n )  =/=  0 )  <->  ( -.  0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
)  \/  ( P `
 n )  =  0 ) )
201196, 200syl6bb 265 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... N )  ->  ( -.  A. b  e.  {
n }  ( 0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
)  <->  ( -.  0  <_  ( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
)  \/  ( P `
 n )  =  0 ) ) )
202191, 201sylibd 218 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... N )  ->  (
( ( ( n  -  1 )  =  0  \/  ( ( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) ) )  /\  -.  A. b  e.  ( 1 ... n ) ( 0  <_  ( ( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) )  ->  ( -.  0  <_  ( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
)  \/  ( P `
 n )  =  0 ) ) )
203145, 202syld 46 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  sup (
( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( P `  b )  =/=  0
) } ) ,  RR ,  <  )  ->  ( -.  0  <_ 
( ( F `  ( P  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  n
)  \/  ( P `
 n )  =  0 ) ) )
204203ad2antlr 732 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  n  e.  (
1 ... N ) )  /\  j  e.  ( 0 ... N ) )  ->  ( (
n  -  1 )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  ( P  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( P `  b )  =/=  0 ) } ) ,  RR ,  <  )  ->  ( -.  0  <_  ( ( F `
 ( P  oF  /  ( (
1 ... N )  X. 
{ k } ) ) ) `  n
)  \/  ( P `
 n )  =  0 ) ) )
205 poimir.1 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F  e.  ( ( Rt  I )  Cn  R
) )
206 poimir.r . . . . . . . . . . . . . . . . . . . . . 22  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
207 retop 21774 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( topGen ` 
ran  (,) )  e.  Top
208207fconst6 5788 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Top
209 pttop 20589 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) --> Top )  ->  ( Xt_ `  ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) )  e.  Top )
21029, 208, 209mp2an 677 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Xt_ `  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) )  e. 
Top
211206, 210eqeltri 2507 . . . . . . . . . . . . . . . . . . . . 21  |-  R  e. 
Top
212 poimir.i . . . . . . . . . . . . . . . . . . . . . 22  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
213 reex 9632 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  e.  _V
214 unitssre 11781 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0 [,] 1 )  C_  RR
215 mapss 7520 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( RR  e.  _V  /\  ( 0 [,] 1
)  C_  RR )  ->  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) 
C_  ( RR  ^m  ( 1 ... N
) ) )
216213, 214, 215mp2an 677 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  C_  ( RR  ^m  (
1 ... N ) )
217212, 216eqsstri 3495 . . . . . . . . . . . . . . . . . . . . 21  |-  I  C_  ( RR  ^m  (
1 ... N ) )
218 uniretop 21775 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  RR  =  U. ( topGen `  ran  (,) )
219206, 218ptuniconst 20605 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( topGen `  ran  (,) )  e.  Top )  ->  ( RR  ^m  ( 1 ... N ) )  = 
U. R )
22029, 207, 219mp2an 677 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( RR 
^m  ( 1 ... N ) )  = 
U. R
221220restuni 20170 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  Top  /\  I  C_  ( RR  ^m  ( 1 ... N
) ) )  ->  I  =  U. ( Rt  I ) )
222211, 217, 221mp2an 677 . . . . . . . . . . . . . . . . . . . 20  |-  I  = 
U. ( Rt  I )
223222, 220cnf 20254 . . . . . . . . . . . . . . . . . . 19  |-  ( F  e.  ( ( Rt  I )  Cn  R )  ->  F : I --> ( RR  ^m  (
1 ... N ) ) )
224205, 223syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : I --> ( RR 
^m  ( 1 ... N ) ) )
225224ad2antrr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  F : I --> ( RR 
^m  ( 1 ... N ) ) )
226 simplr 761 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  k  e.  NN )
227 elfzelz 11802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( 0 ... k )  ->  x  e.  ZZ )
228227zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( 0 ... k )  ->  x  e.  RR )
229228adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  x  e.  RR )
230 nnre 10618 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  NN  ->  k  e.  RR )
231230adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  k  e.  RR )
232 nnne0 10644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  NN  ->  k  =/=  0 )
233232adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  k  =/=  0 )
234229, 231, 233redivcld 10437 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( x  /  k
)  e.  RR )
235 elfzle1 11804 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( 0 ... k )  ->  0  <_  x )
236228, 235jca 535 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( 0 ... k )  ->  (
x  e.  RR  /\  0  <_  x ) )
237 nnrp 11313 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  NN  ->  k  e.  RR+ )
238237rpregt0d 11349 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  NN  ->  (
k  e.  RR  /\  0  <  k ) )
239 divge0 10476 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  RR  /\  0  <_  x )  /\  ( k  e.  RR  /\  0  <  k ) )  ->  0  <_  ( x  /  k ) )
240236, 238, 239syl2an 480 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  0  <_  ( x  /  k ) )
241 elfzle2 11805 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( 0 ... k )  ->  x  <_  k )
242241adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  x  <_  k )
243 1red 9660 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  1  e.  RR )
244237adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  k  e.  RR+ )
245229, 243, 244ledivmuld 11393 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( ( x  / 
k )  <_  1  <->  x  <_  ( k  x.  1 ) ) )
246 nncn 10619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  NN  ->  k  e.  CC )
247246mulid1d 9662 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  NN  ->  (
k  x.  1 )  =  k )
248247breq2d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  NN  ->  (
x  <_  ( k  x.  1 )  <->  x  <_  k ) )
249248adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( x  <_  (
k  x.  1 )  <-> 
x  <_  k )
)
250245, 249bitrd 257 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( ( x  / 
k )  <_  1  <->  x  <_  k ) )
251242, 250mpbird 236 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( x  /  k
)  <_  1 )
25239, 17elicc2i 11702 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  /  k )  e.  ( 0 [,] 1 )  <->  ( (
x  /  k )  e.  RR  /\  0  <_  ( x  /  k
)  /\  ( x  /  k )  <_ 
1 ) )
253234, 240, 251, 252syl3anbrc 1190 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( x  /  k
)  e.  ( 0 [,] 1 ) )
254253ancoms 455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN  /\  x  e.  ( 0 ... k ) )  ->  ( x  / 
k )  e.  ( 0 [,] 1 ) )
255 elsni 4022 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  { k }  ->  y  =  k )
256255oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  { k }  ->  ( x  / 
y )  =  ( x  /  k ) )
257256eleq1d 2492 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  { k }  ->  ( ( x  /  y )  e.  ( 0 [,] 1
)  <->  ( x  / 
k )  e.  ( 0 [,] 1 ) ) )
258254, 257syl5ibrcom 226 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN  /\  x  e.  ( 0 ... k ) )  ->  ( y  e. 
{ k }  ->  ( x  /  y )  e.  ( 0 [,] 1 ) ) )
259258impr 624 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN  /\  ( x  e.  (
0 ... k )  /\  y  e.  { k } ) )  -> 
( x  /  y
)  e.  ( 0 [,] 1 ) )
260226, 259sylan 474 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  ( x  e.  ( 0 ... k
)  /\  y  e.  { k } ) )  ->  ( x  / 
y )  e.  ( 0 [,] 1 ) )
261 elun 3607 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( { 1 }  u.  { 0 } )  <->  ( y  e.  { 1 }  \/  y  e.  { 0 } ) )
262