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

Theorem poimirlem32 31880
Description: Lemma for poimir 31881, combining poimirlem28 31876, poimirlem30 31878, and poimirlem31 31879 to get Equation (1) 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 )
poimir.3  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  z  e.  I  /\  ( z `  n )  =  1 ) )  ->  0  <_  ( ( F `  z ) `  n
) )
Assertion
Ref Expression
poimirlem32  |-  ( ph  ->  E. c  e.  I  A. n  e.  (
1 ... N ) A. v  e.  ( Rt  I
) ( c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
) )
Distinct variable groups:    z, n, ph    n, F    n, N    ph, z    z, F    z, N    n, c, r, v, z, ph    F, c, r, v    I,
c, n, r, v, z    N, c, r, v    R, c, n, r, v, z

Proof of Theorem poimirlem32
Dummy variables  f 
i  j  k  m  p  q  s  g  a  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poimir.0 . . . . . . 7  |-  ( ph  ->  N  e.  NN )
21adantr 466 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  N  e.  NN )
3 oveq1 6304 . . . . . . . . . . . . . 14  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) )  =  ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )
43fveq2d 5877 . . . . . . . . . . . . 13  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  =  ( F `
 ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) )
54fveq1d 5875 . . . . . . . . . . . 12  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  =  ( ( F `  ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
) )
65breq2d 4429 . . . . . . . . . . 11  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  <->  0  <_  ( ( F `  ( (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
) ) )
7 fveq1 5872 . . . . . . . . . . . 12  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( p `  b
)  =  ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  b
) )
87neeq1d 2699 . . . . . . . . . . 11  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( ( p `  b )  =/=  0  <->  ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  b
)  =/=  0 ) )
96, 8anbi12d 715 . . . . . . . . . 10  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
)  <->  ( 0  <_ 
( ( F `  ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) `  b )  /\  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  b
)  =/=  0 ) ) )
109ralbidv 2862 . . . . . . . . 9  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
)  <->  A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  b
)  =/=  0 ) ) )
1110rabbidv 3070 . . . . . . . 8  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) }  =  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  b
)  =/=  0 ) } )
1211uneq2d 3617 . . . . . . 7  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( { 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 `  ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) `  b )  /\  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  b
)  =/=  0 ) } ) )
1312supeq1d 7958 . . . . . 6  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 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 ,  <  )  =  sup ( ( { 0 }  u.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  b
)  =/=  0 ) } ) ,  RR ,  <  ) )
141nnnn0d 10921 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  NN0 )
15 0elfz 11883 . . . . . . . . . . 11  |-  ( N  e.  NN0  ->  0  e.  ( 0 ... N
) )
1614, 15syl 17 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ( 0 ... N ) )
1716snssd 4139 . . . . . . . . 9  |-  ( ph  ->  { 0 }  C_  ( 0 ... N
) )
18 ssrab2 3543 . . . . . . . . . . 11  |-  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 ) }  C_  ( 1 ... N )
19 1eluzge0 11198 . . . . . . . . . . . 12  |-  1  e.  ( ZZ>= `  0 )
20 fzss1 11831 . . . . . . . . . . . 12  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
2119, 20ax-mp 5 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  ( 0 ... N
)
2218, 21sstri 3470 . . . . . . . . . 10  |-  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 ) }  C_  ( 0 ... N )
2322a1i 11 . . . . . . . . 9  |-  ( ph  ->  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) }  C_  (
0 ... N ) )
2417, 23unssd 3639 . . . . . . . 8  |-  ( ph  ->  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) } )  C_  ( 0 ... N
) )
25 ltso 9710 . . . . . . . . 9  |-  <  Or  RR
26 snfi 7649 . . . . . . . . . . 11  |-  { 0 }  e.  Fin
27 fzfi 12178 . . . . . . . . . . . 12  |-  ( 1 ... N )  e. 
Fin
28 rabfi 7794 . . . . . . . . . . . 12  |-  ( ( 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 )
2927, 28ax-mp 5 . . . . . . . . . . 11  |-  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 ) }  e.  Fin
30 unfi 7836 . . . . . . . . . . 11  |-  ( ( { 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 )
3126, 29, 30mp2an 676 . . . . . . . . . 10  |-  ( { 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
32 c0ex 9633 . . . . . . . . . . . 12  |-  0  e.  _V
3332snid 4021 . . . . . . . . . . 11  |-  0  e.  { 0 }
34 elun1 3630 . . . . . . . . . . 11  |-  ( 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
) } ) )
35 ne0i 3764 . . . . . . . . . . 11  |-  ( 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
) } )  =/=  (/) )
3633, 34, 35mp2b 10 . . . . . . . . . 10  |-  ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } )  =/=  (/)
37 0red 9640 . . . . . . . . . . . . 13  |-  ( (
ph  ->  N  e.  NN )  ->  0  e.  RR )
3837snssd 4139 . . . . . . . . . . . 12  |-  ( (
ph  ->  N  e.  NN )  ->  { 0 } 
C_  RR )
391, 38ax-mp 5 . . . . . . . . . . 11  |-  { 0 }  C_  RR
40 elfzelz 11794 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ZZ )
4140ssriv 3465 . . . . . . . . . . . . 13  |-  ( 1 ... N )  C_  ZZ
42 zssre 10940 . . . . . . . . . . . . 13  |-  ZZ  C_  RR
4341, 42sstri 3470 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  RR
4418, 43sstri 3470 . . . . . . . . . . 11  |-  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 ) }  C_  RR
4539, 44unssi 3638 . . . . . . . . . 10  |-  ( { 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
4631, 36, 453pm3.2i 1183 . . . . . . . . 9  |-  ( ( { 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 )
47 fisupcl 7983 . . . . . . . . 9  |-  ( (  <  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
) } ) )
4825, 46, 47mp2an 676 . . . . . . . 8  |-  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
) } )
49 ssel 3455 . . . . . . . 8  |-  ( ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } )  C_  ( 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 ,  <  )  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 ... N ) ) )
5024, 48, 49mpisyl 22 . . . . . . 7  |-  ( ph  ->  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 ... N
) )
5150ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  p : ( 1 ... N ) --> ( 0 ... k ) )  ->  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 ... N
) )
52 elfznn 11822 . . . . . . . . 9  |-  ( n  e.  ( 1 ... N )  ->  n  e.  NN )
53 nngt0 10634 . . . . . . . . . . . 12  |-  ( n  e.  NN  ->  0  <  n )
5453adantr 466 . . . . . . . . . . 11  |-  ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  ->  0  <  n
)
55 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 )  ->  ( p `  b )  =/=  0
)
5655ralimi 2816 . . . . . . . . . . . . 13  |-  ( A. b  e.  ( 1 ... s ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 )  ->  A. b  e.  ( 1 ... s ) ( p `  b
)  =/=  0 )
57 elfznn 11822 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 1 ... N )  ->  s  e.  NN )
58 nnre 10612 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  RR )
59 nnre 10612 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  NN  ->  s  e.  RR )
60 lenlt 9708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  RR  /\  s  e.  RR )  ->  ( n  <_  s  <->  -.  s  <  n ) )
6158, 59, 60syl2an 479 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN  /\  s  e.  NN )  ->  ( n  <_  s  <->  -.  s  <  n ) )
62 elfz1b 11858 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... s )  <->  ( n  e.  NN  /\  s  e.  NN  /\  n  <_ 
s ) )
6362biimpri 209 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  s  e.  NN  /\  n  <_  s )  ->  n  e.  ( 1 ... s
) )
64633expia 1207 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN  /\  s  e.  NN )  ->  ( n  <_  s  ->  n  e.  ( 1 ... s ) ) )
6561, 64sylbird 238 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN  /\  s  e.  NN )  ->  ( -.  s  < 
n  ->  n  e.  ( 1 ... s
) ) )
66 fveq2 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  n  ->  (
p `  b )  =  ( p `  n ) )
6766eqeq1d 2422 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  n  ->  (
( p `  b
)  =  0  <->  (
p `  n )  =  0 ) )
6867rspcev 3179 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  ( 1 ... s )  /\  ( p `  n
)  =  0 )  ->  E. b  e.  ( 1 ... s ) ( p `  b
)  =  0 )
6968expcom 436 . . . . . . . . . . . . . . . . . 18  |-  ( ( p `  n )  =  0  ->  (
n  e.  ( 1 ... s )  ->  E. b  e.  (
1 ... s ) ( p `  b )  =  0 ) )
7065, 69sylan9 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( n  e.  NN  /\  s  e.  NN )  /\  ( p `  n )  =  0 )  ->  ( -.  s  <  n  ->  E. b  e.  ( 1 ... s
) ( p `  b )  =  0 ) )
7170an32s 811 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  /\  s  e.  NN )  ->  ( -.  s  <  n  ->  E. b  e.  ( 1 ... s
) ( p `  b )  =  0 ) )
72 nne 2622 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( p `  b
)  =/=  0  <->  (
p `  b )  =  0 )
7372rexbii 2925 . . . . . . . . . . . . . . . . 17  |-  ( E. b  e.  ( 1 ... s )  -.  ( p `  b
)  =/=  0  <->  E. b  e.  ( 1 ... s ) ( p `  b )  =  0 )
74 rexnal 2871 . . . . . . . . . . . . . . . . 17  |-  ( E. b  e.  ( 1 ... s )  -.  ( p `  b
)  =/=  0  <->  -.  A. b  e.  ( 1 ... s ) ( p `  b )  =/=  0 )
7573, 74bitr3i 254 . . . . . . . . . . . . . . . 16  |-  ( E. b  e.  ( 1 ... s ) ( p `  b )  =  0  <->  -.  A. b  e.  ( 1 ... s
) ( p `  b )  =/=  0
)
7671, 75syl6ib 229 . . . . . . . . . . . . . . 15  |-  ( ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  /\  s  e.  NN )  ->  ( -.  s  <  n  ->  -.  A. b  e.  ( 1 ... s
) ( p `  b )  =/=  0
) )
7776con4d 108 . . . . . . . . . . . . . 14  |-  ( ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  /\  s  e.  NN )  ->  ( A. b  e.  ( 1 ... s
) ( p `  b )  =/=  0  ->  s  <  n ) )
7857, 77sylan2 476 . . . . . . . . . . . . 13  |-  ( ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  /\  s  e.  ( 1 ... N ) )  ->  ( A. b  e.  ( 1 ... s ) ( p `  b )  =/=  0  ->  s  <  n ) )
7956, 78syl5 33 . . . . . . . . . . . 12  |-  ( ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  /\  s  e.  ( 1 ... N ) )  ->  ( A. b  e.  ( 1 ... s ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 )  ->  s  <  n
) )
8079ralrimiva 2837 . . . . . . . . . . 11  |-  ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  ->  A. s  e.  ( 1 ... N ) ( A. b  e.  ( 1 ... s
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
)  ->  s  <  n ) )
81 ralunb 3644 . . . . . . . . . . . 12  |-  ( A. s  e.  ( {
0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } ) s  <  n  <->  ( A. s  e.  { 0 } s  <  n  /\  A. s  e.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } s  < 
n ) )
82 breq1 4420 . . . . . . . . . . . . . 14  |-  ( s  =  0  ->  (
s  <  n  <->  0  <  n ) )
8332, 82ralsn 4032 . . . . . . . . . . . . 13  |-  ( A. s  e.  { 0 } s  <  n  <->  0  <  n )
84 oveq2 6305 . . . . . . . . . . . . . . 15  |-  ( a  =  s  ->  (
1 ... a )  =  ( 1 ... s
) )
8584raleqdv 3029 . . . . . . . . . . . . . 14  |-  ( a  =  s  ->  ( A. b  e.  (
1 ... a ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 )  <->  A. b  e.  (
1 ... s ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 ) ) )
8685ralrab 3230 . . . . . . . . . . . . 13  |-  ( A. s  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) } s  < 
n  <->  A. s  e.  ( 1 ... N ) ( A. b  e.  ( 1 ... s
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
)  ->  s  <  n ) )
8783, 86anbi12i 701 . . . . . . . . . . . 12  |-  ( ( A. s  e.  {
0 } s  < 
n  /\  A. s  e.  { a  e.  ( 1 ... N )  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) } s  < 
n )  <->  ( 0  <  n  /\  A. s  e.  ( 1 ... N ) ( A. b  e.  ( 1 ... s ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
)  ->  s  <  n ) ) )
8881, 87bitri 252 . . . . . . . . . . 11  |-  ( A. s  e.  ( {
0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } ) s  <  n  <->  ( 0  <  n  /\  A. s  e.  ( 1 ... N ) ( A. b  e.  ( 1 ... s ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
)  ->  s  <  n ) ) )
8954, 80, 88sylanbrc 668 . . . . . . . . . 10  |-  ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  ->  A. s  e.  ( { 0 }  u.  { a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } ) s  <  n )
90 breq1 4420 . . . . . . . . . . 11  |-  ( s  =  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 ,  <  )  ->  ( s  <  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
) )
9190rspcva 3177 . . . . . . . . . 10  |-  ( ( 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
) } )  /\  A. s  e.  ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } ) s  <  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
)
9248, 89, 91sylancr 667 . . . . . . . . 9  |-  ( ( n  e.  NN  /\  ( p `  n
)  =  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 ,  <  )  <  n )
9352, 92sylan 473 . . . . . . . 8  |-  ( ( n  e.  ( 1 ... N )  /\  ( p `  n
)  =  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 ,  <  )  <  n )
94933adant2 1024 . . . . . . 7  |-  ( ( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  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 ,  <  )  <  n )
9594adantl 467 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  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 ,  <  )  <  n )
9640zred 11036 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... N )  ->  n  e.  RR )
97963ad2ant1 1026 . . . . . . . . . 10  |-  ( ( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k )  ->  n  e.  RR )
9897adantl 467 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  n  e.  RR )
99 simpr1 1011 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  n  e.  ( 1 ... N
) )
100 simpll 758 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ph )
101 simplr 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  k  e.  NN )
102 elfzelz 11794 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0 ... k )  ->  i  e.  ZZ )
103102zred 11036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0 ... k )  ->  i  e.  RR )
104 nndivre 10641 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  RR  /\  k  e.  NN )  ->  ( i  /  k
)  e.  RR )
105103, 104sylan 473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( i  /  k
)  e.  RR )
106 elfzle1 11796 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0 ... k )  ->  0  <_  i )
107103, 106jca 534 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0 ... k )  ->  (
i  e.  RR  /\  0  <_  i ) )
108 nnrp 11307 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  NN  ->  k  e.  RR+ )
109108rpregt0d 11343 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN  ->  (
k  e.  RR  /\  0  <  k ) )
110 divge0 10470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( i  e.  RR  /\  0  <_  i )  /\  ( k  e.  RR  /\  0  <  k ) )  ->  0  <_  ( i  /  k ) )
111107, 109, 110syl2an 479 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  0  <_  ( i  /  k ) )
112 elfzle2 11797 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0 ... k )  ->  i  <_  k )
113112adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  i  <_  k )
114103adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  i  e.  RR )
115 1red 9654 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  1  e.  RR )
116108adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  k  e.  RR+ )
117114, 115, 116ledivmuld 11387 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( ( i  / 
k )  <_  1  <->  i  <_  ( k  x.  1 ) ) )
118 nncn 10613 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  NN  ->  k  e.  CC )
119118mulid1d 9656 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  NN  ->  (
k  x.  1 )  =  k )
120119breq2d 4429 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  NN  ->  (
i  <_  ( k  x.  1 )  <->  i  <_  k ) )
121120adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( i  <_  (
k  x.  1 )  <-> 
i  <_  k )
)
122117, 121bitrd 256 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( ( i  / 
k )  <_  1  <->  i  <_  k ) )
123113, 122mpbird 235 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( i  /  k
)  <_  1 )
124 0re 9639 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
125 1re 9638 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR
126124, 125elicc2i 11696 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  /  k )  e.  ( 0 [,] 1 )  <->  ( (
i  /  k )  e.  RR  /\  0  <_  ( i  /  k
)  /\  ( i  /  k )  <_ 
1 ) )
127105, 111, 123, 126syl3anbrc 1189 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( i  /  k
)  e.  ( 0 [,] 1 ) )
128127ancoms 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  i  e.  ( 0 ... k ) )  ->  ( i  / 
k )  e.  ( 0 [,] 1 ) )
129 elsni 4018 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  { k }  ->  j  =  k )
130129oveq2d 6313 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  { k }  ->  ( i  / 
j )  =  ( i  /  k ) )
131130eleq1d 2489 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  { k }  ->  ( ( i  /  j )  e.  ( 0 [,] 1
)  <->  ( i  / 
k )  e.  ( 0 [,] 1 ) ) )
132128, 131syl5ibrcom 225 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  i  e.  ( 0 ... k ) )  ->  ( j  e. 
{ k }  ->  ( i  /  j )  e.  ( 0 [,] 1 ) ) )
133132impr 623 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  ( i  e.  ( 0 ... k )  /\  j  e.  {
k } ) )  ->  ( i  / 
j )  e.  ( 0 [,] 1 ) )
134101, 133sylan 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  ( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k
) ) )  /\  ( i  e.  ( 0 ... k )  /\  j  e.  {
k } ) )  ->  ( i  / 
j )  e.  ( 0 [,] 1 ) )
135 simprr 764 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  p :
( 1 ... N
) --> ( 0 ... k ) )
136 vex 3081 . . . . . . . . . . . . . . . . . 18  |-  k  e. 
_V
137136fconst 5778 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... N )  X.  { k } ) : ( 1 ... N ) --> { k }
138137a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  ( (
1 ... N )  X. 
{ k } ) : ( 1 ... N ) --> { k } )
139 fzfid 12179 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  ( 1 ... N )  e. 
Fin )
140 inidm 3668 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
141134, 135, 138, 139, 139, 140off 6552 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) : ( 1 ... N
) --> ( 0 [,] 1 ) )
142 poimir.i . . . . . . . . . . . . . . . . 17  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
143142eleq2i 2498 . . . . . . . . . . . . . . . 16  |-  ( ( p  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  I  <->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) )
144 ovex 6325 . . . . . . . . . . . . . . . . 17  |-  ( 0 [,] 1 )  e. 
_V
145 ovex 6325 . . . . . . . . . . . . . . . . 17  |-  ( 1 ... N )  e. 
_V
146144, 145elmap 7500 . . . . . . . . . . . . . . . 16  |-  ( ( p  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  ( ( 0 [,] 1 )  ^m  ( 1 ... N
) )  <->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) : ( 1 ... N
) --> ( 0 [,] 1 ) )
147143, 146bitri 252 . . . . . . . . . . . . . . 15  |-  ( ( p  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  I  <->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) : ( 1 ... N
) --> ( 0 [,] 1 ) )
148141, 147sylibr 215 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  I )
1491483adantr3 1166 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  I )
150 3anass 986 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k )  <-> 
( n  e.  ( 1 ... N )  /\  ( p : ( 1 ... N
) --> ( 0 ... k )  /\  (
p `  n )  =  k ) ) )
151 ancom 451 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  ( 1 ... N )  /\  ( p : ( 1 ... N ) --> ( 0 ... k
)  /\  ( p `  n )  =  k ) )  <->  ( (
p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n )  =  k )  /\  n  e.  ( 1 ... N
) ) )
152150, 151bitri 252 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k )  <-> 
( ( p : ( 1 ... N
) --> ( 0 ... k )  /\  (
p `  n )  =  k )  /\  n  e.  ( 1 ... N ) ) )
153 ffn 5738 . . . . . . . . . . . . . . . . . 18  |-  ( p : ( 1 ... N ) --> ( 0 ... k )  ->  p  Fn  ( 1 ... N ) )
154153ad2antrl 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n )  =  k ) )  ->  p  Fn  ( 1 ... N
) )
155 fnconstg 5780 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  _V  ->  (
( 1 ... N
)  X.  { k } )  Fn  (
1 ... N ) )
156136, 155mp1i 13 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n )  =  k ) )  ->  (
( 1 ... N
)  X.  { k } )  Fn  (
1 ... N ) )
157 fzfid 12179 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n )  =  k ) )  ->  (
1 ... N )  e. 
Fin )
158 simplrr 769 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  ( p : ( 1 ... N ) --> ( 0 ... k
)  /\  ( p `  n )  =  k ) )  /\  n  e.  ( 1 ... N
) )  ->  (
p `  n )  =  k )
159136fvconst2 6127 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
k } ) `  n )  =  k )
160159adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  ( p : ( 1 ... N ) --> ( 0 ... k
)  /\  ( p `  n )  =  k ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( 1 ... N )  X.  {
k } ) `  n )  =  k )
161154, 156, 157, 157, 140, 158, 160ofval 6546 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  ( p : ( 1 ... N ) --> ( 0 ... k
)  /\  ( p `  n )  =  k ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) `  n )  =  ( k  / 
k ) )
162161anasss 651 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
( p : ( 1 ... N ) --> ( 0 ... k
)  /\  ( p `  n )  =  k )  /\  n  e.  ( 1 ... N
) ) )  -> 
( ( p  oF  /  ( ( 1 ... N )  X.  { k } ) ) `  n
)  =  ( k  /  k ) )
163152, 162sylan2b 477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 n )  =  ( k  /  k
) )
164 nnne0 10638 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  =/=  0 )
165118, 164dividd 10377 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  (
k  /  k )  =  1 )
166165ad2antlr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( k  /  k )  =  1 )
167163, 166eqtrd 2461 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 n )  =  1 )
168 ovex 6325 . . . . . . . . . . . . . 14  |-  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e. 
_V
169 eleq1 2492 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
z  e.  I  <->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  I ) )
170 fveq1 5872 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
z `  n )  =  ( ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) `  n ) )
171170eqeq1d 2422 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
( z `  n
)  =  1  <->  (
( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) `  n )  =  1 ) )
172169, 1713anbi23d 1338 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
( n  e.  ( 1 ... N )  /\  z  e.  I  /\  ( z `  n
)  =  1 )  <-> 
( n  e.  ( 1 ... N )  /\  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  e.  I  /\  ( ( p  oF  /  ( ( 1 ... N )  X.  { k } ) ) `  n
)  =  1 ) ) )
173172anbi2d 708 . . . . . . . . . . . . . . 15  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
( ph  /\  (
n  e.  ( 1 ... N )  /\  z  e.  I  /\  ( z `  n
)  =  1 ) )  <->  ( ph  /\  ( n  e.  (
1 ... N )  /\  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) )  e.  I  /\  ( ( p  oF  /  ( ( 1 ... N )  X.  { k } ) ) `  n
)  =  1 ) ) ) )
174 fveq2 5873 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  ( F `  z )  =  ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) )
175174fveq1d 5875 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
( F `  z
) `  n )  =  ( ( F `
 ( p  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) `  n ) )
176175breq2d 4429 . . . . . . . . . . . . . . 15  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
0  <_  ( ( F `  z ) `  n )  <->  0  <_  ( ( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  n ) ) )
177173, 176imbi12d 321 . . . . . . . . . . . . . 14  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
( ( ph  /\  ( n  e.  (
1 ... N )  /\  z  e.  I  /\  ( z `  n
)  =  1 ) )  ->  0  <_  ( ( F `  z
) `  n )
)  <->  ( ( ph  /\  ( n  e.  ( 1 ... N )  /\  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  e.  I  /\  ( ( p  oF  /  ( ( 1 ... N )  X.  { k } ) ) `  n
)  =  1 ) )  ->  0  <_  ( ( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  n ) ) ) )
178 poimir.3 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  z  e.  I  /\  ( z `  n )  =  1 ) )  ->  0  <_  ( ( F `  z ) `  n
) )
179168, 177, 178vtocl 3130 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  I  /\  ( ( p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 n )  =  1 ) )  -> 
0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 n ) )
180100, 99, 149, 167, 179syl13anc 1266 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  0  <_  ( ( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  n ) )
181 simpr 462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
182 simp3 1007 . . . . . . . . . . . . 13  |-  ( ( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k )  ->  ( p `  n )  =  k )
183 neeq1 2703 . . . . . . . . . . . . . . 15  |-  ( ( p `  n )  =  k  ->  (
( p `  n
)  =/=  0  <->  k  =/=  0 ) )
184164, 183syl5ibrcom 225 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  (
( p `  n
)  =  k  -> 
( p `  n
)  =/=  0 ) )
185184imp 430 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  /\  ( p `  n
)  =  k )  ->  ( p `  n )  =/=  0
)
186181, 182, 185syl2an 479 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( p `  n )  =/=  0
)
187 vex 3081 . . . . . . . . . . . . 13  |-  n  e. 
_V
188 fveq2 5873 . . . . . . . . . . . . . . 15  |-  ( b  =  n  ->  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  =  ( ( F `
 ( p  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) `  n ) )
189188breq2d 4429 . . . . . . . . . . . . . 14  |-  ( b  =  n  ->  (
0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  <->  0  <_  ( ( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  n ) ) )
19066neeq1d 2699 . . . . . . . . . . . . . 14  |-  ( b  =  n  ->  (
( p `  b
)  =/=  0  <->  (
p `  n )  =/=  0 ) )
191189, 190anbi12d 715 . . . . . . . . . . . . 13  |-  ( 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
) ) )
192187, 191ralsn 4032 . . . . . . . . . . . 12  |-  ( 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
) )
193180, 186, 192sylanbrc 668 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  A. b  e.  { n }  (
0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 ) )
19440zcnd 11037 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  n  e.  CC )
195 1cnd 9655 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  1  e.  CC )
196194, 195subeq0ad 9992 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  0  <->  n  =  1 ) )
197196biimpcd 227 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  =  0  ->  (
n  e.  ( 1 ... N )  ->  n  =  1 ) )
198 1z 10963 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  ZZ
199 fzsn 11834 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
200198, 199ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... 1 )  =  { 1 }
201 oveq2 6305 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
1 ... n )  =  ( 1 ... 1
) )
202 sneq 4003 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  { n }  =  { 1 } )
203200, 201, 2023eqtr4a 2487 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
1 ... n )  =  { n } )
204203raleqdv 3029 . . . . . . . . . . . . . . . . . 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
) ) )
205204biimprd 226 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( 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
) ) )
206197, 205syl6 34 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  =  0  ->  (
n  e.  ( 1 ... N )  -> 
( 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
) ) ) )
207 ralun 3645 . . . . . . . . . . . . . . . . . . . 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 ) )
208 npcan1 10040 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  CC  ->  (
( n  -  1 )  +  1 )  =  n )
209194, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  +  1 )  =  n )
210 elfzuz 11790 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ( ZZ>= `  1 )
)
211209, 210eqeltrd 2508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  +  1 )  e.  ( ZZ>= `  1
) )
212 peano2zm 10976 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  ZZ  ->  (
n  -  1 )  e.  ZZ )
213 uzid 11169 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  -  1 )  e.  ZZ  ->  (
n  -  1 )  e.  ( ZZ>= `  (
n  -  1 ) ) )
214 peano2uz 11208 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  -  1 )  e.  ( ZZ>= `  (
n  -  1 ) )  ->  ( (
n  -  1 )  +  1 )  e.  ( ZZ>= `  ( n  -  1 ) ) )
21540, 212, 213, 2144syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  +  1 )  e.  ( ZZ>= `  (
n  -  1 ) ) )
216209, 215eqeltrrd 2509 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ( ZZ>= `  ( n  -  1 ) ) )
217 fzsplit2 11818 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( n  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  n  e.  ( ZZ>= `  ( n  -  1 ) ) )  ->  ( 1 ... n )  =  ( ( 1 ... ( n  -  1 ) )  u.  (
( ( n  - 
1 )  +  1 ) ... n ) ) )
218211, 216, 217syl2anc 665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( 1 ... N )  ->  (
1 ... n )  =  ( ( 1 ... ( n  -  1 ) )  u.  (
( ( n  - 
1 )  +  1 ) ... n ) ) )
219209oveq1d 6312 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
( ( n  - 
1 )  +  1 ) ... n )  =  ( n ... n ) )
220 fzsn 11834 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  ZZ  ->  (
n ... n )  =  { n } )
22140, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
n ... n )  =  { n } )
222219, 221eqtrd 2461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  (
( ( n  - 
1 )  +  1 ) ... n )  =  { n }
)
223222uneq2d 3617 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( 1 ... N )  ->  (
( 1 ... (
n  -  1 ) )  u.  ( ( ( n  -  1 )  +  1 ) ... n ) )  =  ( ( 1 ... ( n  - 
1 ) )  u. 
{ n } ) )
224218, 223eqtrd 2461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... N )  ->  (
1 ... n )  =  ( ( 1 ... ( n  -  1 ) )  u.  {
n } ) )
225224raleqdv 3029 . . . . . . . . . . . . . . . . . . . 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 ) ) )
226207, 225syl5ibr 224 . . . . . . . . . . . . . . . . . . 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
) ) )
227226expd 437 . . . . . . . . . . . . . . . . . 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
) ) ) )
228227com12 32 . . . . . . . . . . . . . . . . 17  |-  ( A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 )  ->  ( n  e.  ( 1 ... N
)  ->  ( 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
) ) ) )
229228adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  -  1 )  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... ( n  - 
1 ) ) ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 ) )  ->  ( n  e.  ( 1 ... N
)  ->  ( 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
) ) ) )
230206, 229jaoi 380 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) )  -> 
( n  e.  ( 1 ... N )  ->  ( 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
) ) ) )
231230imdistand 696 . . . . . . . . . . . . . 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
) ) )  -> 
( ( n  e.  ( 1 ... N
)  /\  A. b  e.  { 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
) ) ) )
232231com12 32 . . . . . . . . . . . . 13  |-  ( ( n  e.  ( 1 ... N )  /\  A. b  e.  { n }  ( 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
) ) )  -> 
( n  e.  ( 1 ... N )  /\  A. b  e.  ( 1 ... n
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) ) ) )
233 elun 3603 . . . . . . . . . . . . . 14  |-  ( ( 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
) } ) )
234 ovex 6325 . . . . . . . . . . . . . . . 16  |-  ( n  -  1 )  e. 
_V
235234elsnc 4017 . . . . . . . . . . . . . . 15  |-  ( ( n  -  1 )  e.  { 0 }  <-> 
( n  -  1 )  =  0 )
236 oveq2 6305 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( n  - 
1 )  ->  (
1 ... a )  =  ( 1 ... (
n  -  1 ) ) )
237236raleqdv 3029 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) )
238237elrab 3226 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) )
239235, 238orbi12i 523 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
240233, 239bitri 252 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) )
241 oveq2 6305 . . . . . . . . . . . . . . 15  |-  ( a  =  n  ->  (
1 ... a )  =  ( 1 ... n
) )
242241raleqdv 3029 . . . . . . . . . . . . . 14  |-  ( 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 ) ) )
243242elrab 3226 . . . . . . . . . . . . 13  |-  ( 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
) ) )
244232, 240, 2433imtr4g 273 . . . . . . . . . . . 12  |-  ( ( n  e.  ( 1 ... N )  /\  A. b  e.  { n }  ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) )  ->  (
( 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  e.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) } ) )
245 elun2 3631 . . . . . . . . . . . 12  |-  ( 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
) } ) )
246244, 245syl6 34 . . . . . . . . . . 11  |-  ( ( n  e.  ( 1 ... N )  /\  A. b  e.  { n }  ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) )  ->  (
( 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  e.  ( {
0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } ) ) )
24799, 193, 246syl2anc 665 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( (
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  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) } ) ) )
248 fimaxre2 10548 . . . . . . . . . . . . 13  |-  ( ( ( { 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. i  e.  RR  A. j  e.  ( { 0 }  u.  {
a  e.  ( 1 ... N )  | 
A. b  e.  ( 1 ... a ) ( 0  <_  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  /\  ( p `  b )  =/=  0
) } ) j  <_  i )
24945, 31, 248mp2an 676 . . . . . . . . . . . 12  |-  E. i  e.  RR  A. j  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) } ) j  <_  i
25045, 36, 2493pm3.2i 1183 . . . . . . . . . . 11  |-  ( ( { 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. i  e.  RR  A. j  e.  ( { 0 }  u.  { a  e.  ( 1 ... N
)  |  A. b  e.  ( 1 ... a
) ( 0  <_ 
( ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) `  b
)  /\  ( p `  b )  =/=  0
) } ) j  <_  i )
251250suprubii 10578 . . . . . . . . . 10  |-  ( 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 ,  <  )
)
252247, 251syl6 34 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( (
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  <_  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 ,  <  )
) )
253 ltm1 10441 . . . . . . . . . 10  |-  ( n  e.  RR  ->  (
n  -  1 )  <  n )
254 peano2rem 9937 . . . . . . . . . . 11  |-  ( n  e.  RR  ->  (
n  -  1 )  e.  RR )
25545, 48sselii 3458 . . . . . . . . . . . 12  |-  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.  RR
256 ltletr 9721 . . . . . . . . . . . 12  |-  ( ( ( n  -  1 )  e.  RR  /\  n  e.  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.  RR )  ->  ( ( ( n  -  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 ,  <  )
)  ->  ( 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 ,  <  ) ) )
257255, 256mp3an3 1349 . . . . . . . . . . 11  |-  ( ( ( n  -  1 )  e.  RR  /\  n  e.  RR )  ->  ( ( ( n  -  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 ) } )