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

Theorem poimirlem32 31965
Description: Lemma for poimir 31966, combining poimirlem28 31961, poimirlem30 31963, and poimirlem31 31964 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 467 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  N  e.  NN )
3 oveq1 6295 . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . 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 5865 . . . . . . . . . . . 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 4413 . . . . . . . . . . 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 5862 . . . . . . . . . . . 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 2682 . . . . . . . . . . 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 716 . . . . . . . . . 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 2826 . . . . . . . . 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 3035 . . . . . . . 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 3587 . . . . . . 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 7957 . . . . . 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 10922 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  NN0 )
15 0elfz 11886 . . . . . . . . . . 11  |-  ( N  e.  NN0  ->  0  e.  ( 0 ... N
) )
1614, 15syl 17 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ( 0 ... N ) )
1716snssd 4116 . . . . . . . . 9  |-  ( ph  ->  { 0 }  C_  ( 0 ... N
) )
18 ssrab2 3513 . . . . . . . . . . 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 11199 . . . . . . . . . . . 12  |-  1  e.  ( ZZ>= `  0 )
20 fzss1 11834 . . . . . . . . . . . 12  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
2119, 20ax-mp 5 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  ( 0 ... N
)
2218, 21sstri 3440 . . . . . . . . . 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 3609 . . . . . . . 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 9711 . . . . . . . . 9  |-  <  Or  RR
26 snfi 7647 . . . . . . . . . . 11  |-  { 0 }  e.  Fin
27 fzfi 12182 . . . . . . . . . . . 12  |-  ( 1 ... N )  e. 
Fin
28 rabfi 7793 . . . . . . . . . . . 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 7835 . . . . . . . . . . 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 677 . . . . . . . . . 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 9634 . . . . . . . . . . . 12  |-  0  e.  _V
3332snid 3995 . . . . . . . . . . 11  |-  0  e.  { 0 }
34 elun1 3600 . . . . . . . . . . 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 3736 . . . . . . . . . . 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 9641 . . . . . . . . . . . . 13  |-  ( (
ph  ->  N  e.  NN )  ->  0  e.  RR )
3837snssd 4116 . . . . . . . . . . . 12  |-  ( (
ph  ->  N  e.  NN )  ->  { 0 } 
C_  RR )
391, 38ax-mp 5 . . . . . . . . . . 11  |-  { 0 }  C_  RR
40 elfzelz 11797 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ZZ )
4140ssriv 3435 . . . . . . . . . . . . 13  |-  ( 1 ... N )  C_  ZZ
42 zssre 10941 . . . . . . . . . . . . 13  |-  ZZ  C_  RR
4341, 42sstri 3440 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  RR
4418, 43sstri 3440 . . . . . . . . . . 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 3608 . . . . . . . . . 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 1185 . . . . . . . . 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 7982 . . . . . . . . 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 677 . . . . . . . 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 3425 . . . . . . . 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 21 . . . . . . 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 731 . . . . . 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 11825 . . . . . . . . 9  |-  ( n  e.  ( 1 ... N )  ->  n  e.  NN )
53 nngt0 10635 . . . . . . . . . . . 12  |-  ( n  e.  NN  ->  0  <  n )
5453adantr 467 . . . . . . . . . . 11  |-  ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  ->  0  <  n
)
55 simpr 463 . . . . . . . . . . . . . 14  |-  ( ( 0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  /\  ( p `  b
)  =/=  0 )  ->  ( p `  b )  =/=  0
)
5655ralimi 2780 . . . . . . . . . . . . 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 11825 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 1 ... N )  ->  s  e.  NN )
58 nnre 10613 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  RR )
59 nnre 10613 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  NN  ->  s  e.  RR )
60 lenlt 9709 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  RR  /\  s  e.  RR )  ->  ( n  <_  s  <->  -.  s  <  n ) )
6158, 59, 60syl2an 480 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN  /\  s  e.  NN )  ->  ( n  <_  s  <->  -.  s  <  n ) )
62 elfz1b 11861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... s )  <->  ( n  e.  NN  /\  s  e.  NN  /\  n  <_ 
s ) )
6362biimpri 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  s  e.  NN  /\  n  <_  s )  ->  n  e.  ( 1 ... s
) )
64633expia 1209 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN  /\  s  e.  NN )  ->  ( n  <_  s  ->  n  e.  ( 1 ... s ) ) )
6561, 64sylbird 239 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN  /\  s  e.  NN )  ->  ( -.  s  < 
n  ->  n  e.  ( 1 ... s
) ) )
66 fveq2 5863 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  n  ->  (
p `  b )  =  ( p `  n ) )
6766eqeq1d 2452 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  n  ->  (
( p `  b
)  =  0  <->  (
p `  n )  =  0 ) )
6867rspcev 3149 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  ( 1 ... s )  /\  ( p `  n
)  =  0 )  ->  E. b  e.  ( 1 ... s ) ( p `  b
)  =  0 )
6968expcom 437 . . . . . . . . . . . . . . . . . 18  |-  ( ( p `  n )  =  0  ->  (
n  e.  ( 1 ... s )  ->  E. b  e.  (
1 ... s ) ( p `  b )  =  0 ) )
7065, 69sylan9 662 . . . . . . . . . . . . . . . . 17  |-  ( ( ( n  e.  NN  /\  s  e.  NN )  /\  ( p `  n )  =  0 )  ->  ( -.  s  <  n  ->  E. b  e.  ( 1 ... s
) ( p `  b )  =  0 ) )
7170an32s 812 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  /\  s  e.  NN )  ->  ( -.  s  <  n  ->  E. b  e.  ( 1 ... s
) ( p `  b )  =  0 ) )
72 nne 2627 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( p `  b
)  =/=  0  <->  (
p `  b )  =  0 )
7372rexbii 2888 . . . . . . . . . . . . . . . . 17  |-  ( E. b  e.  ( 1 ... s )  -.  ( p `  b
)  =/=  0  <->  E. b  e.  ( 1 ... s ) ( p `  b )  =  0 )
74 rexnal 2835 . . . . . . . . . . . . . . . . 17  |-  ( E. b  e.  ( 1 ... s )  -.  ( p `  b
)  =/=  0  <->  -.  A. b  e.  ( 1 ... s ) ( p `  b )  =/=  0 )
7573, 74bitr3i 255 . . . . . . . . . . . . . . . 16  |-  ( E. b  e.  ( 1 ... s ) ( p `  b )  =  0  <->  -.  A. b  e.  ( 1 ... s
) ( p `  b )  =/=  0
)
7671, 75syl6ib 230 . . . . . . . . . . . . . . 15  |-  ( ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  /\  s  e.  NN )  ->  ( -.  s  <  n  ->  -.  A. b  e.  ( 1 ... s
) ( p `  b )  =/=  0
) )
7776con4d 109 . . . . . . . . . . . . . 14  |-  ( ( ( n  e.  NN  /\  ( p `  n
)  =  0 )  /\  s  e.  NN )  ->  ( A. b  e.  ( 1 ... s
) ( p `  b )  =/=  0  ->  s  <  n ) )
7857, 77sylan2 477 . . . . . . . . . . . . 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 2801 . . . . . . . . . . 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 3614 . . . . . . . . . . . 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 4404 . . . . . . . . . . . . . 14  |-  ( s  =  0  ->  (
s  <  n  <->  0  <  n ) )
8332, 82ralsn 4009 . . . . . . . . . . . . 13  |-  ( A. s  e.  { 0 } s  <  n  <->  0  <  n )
84 oveq2 6296 . . . . . . . . . . . . . . 15  |-  ( a  =  s  ->  (
1 ... a )  =  ( 1 ... s
) )
8584raleqdv 2992 . . . . . . . . . . . . . 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 3199 . . . . . . . . . . . . 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 702 . . . . . . . . . . . 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 253 . . . . . . . . . . 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 669 . . . . . . . . . 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 4404 . . . . . . . . . . 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 3147 . . . . . . . . . 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 668 . . . . . . . . 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 474 . . . . . . . 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 1026 . . . . . . 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 468 . . . . . 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 11037 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... N )  ->  n  e.  RR )
97963ad2ant1 1028 . . . . . . . . . 10  |-  ( ( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k )  ->  n  e.  RR )
9897adantl 468 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  n  e.  RR )
99 simpr1 1013 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  n  e.  ( 1 ... N
) )
100 simpll 759 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ph )
101 simplr 761 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  k  e.  NN )
102 elfzelz 11797 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0 ... k )  ->  i  e.  ZZ )
103102zred 11037 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0 ... k )  ->  i  e.  RR )
104 nndivre 10642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  RR  /\  k  e.  NN )  ->  ( i  /  k
)  e.  RR )
105103, 104sylan 474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( i  /  k
)  e.  RR )
106 elfzle1 11799 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0 ... k )  ->  0  <_  i )
107103, 106jca 535 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0 ... k )  ->  (
i  e.  RR  /\  0  <_  i ) )
108 nnrp 11308 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  NN  ->  k  e.  RR+ )
109108rpregt0d 11344 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN  ->  (
k  e.  RR  /\  0  <  k ) )
110 divge0 10471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( i  e.  RR  /\  0  <_  i )  /\  ( k  e.  RR  /\  0  <  k ) )  ->  0  <_  ( i  /  k ) )
111107, 109, 110syl2an 480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  0  <_  ( i  /  k ) )
112 elfzle2 11800 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0 ... k )  ->  i  <_  k )
113112adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  i  <_  k )
114103adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  i  e.  RR )
115 1red 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  1  e.  RR )
116108adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  k  e.  RR+ )
117114, 115, 116ledivmuld 11388 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( ( i  / 
k )  <_  1  <->  i  <_  ( k  x.  1 ) ) )
118 nncn 10614 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  NN  ->  k  e.  CC )
119118mulid1d 9657 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  NN  ->  (
k  x.  1 )  =  k )
120119breq2d 4413 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  NN  ->  (
i  <_  ( k  x.  1 )  <->  i  <_  k ) )
121120adantl 468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( i  <_  (
k  x.  1 )  <-> 
i  <_  k )
)
122117, 121bitrd 257 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( ( i  / 
k )  <_  1  <->  i  <_  k ) )
123113, 122mpbird 236 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( i  /  k
)  <_  1 )
124 0re 9640 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
125 1re 9639 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR
126124, 125elicc2i 11697 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  /  k )  e.  ( 0 [,] 1 )  <->  ( (
i  /  k )  e.  RR  /\  0  <_  ( i  /  k
)  /\  ( i  /  k )  <_ 
1 ) )
127105, 111, 123, 126syl3anbrc 1191 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0 ... k )  /\  k  e.  NN )  ->  ( i  /  k
)  e.  ( 0 [,] 1 ) )
128127ancoms 455 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  i  e.  ( 0 ... k ) )  ->  ( i  / 
k )  e.  ( 0 [,] 1 ) )
129 elsni 3992 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  { k }  ->  j  =  k )
130129oveq2d 6304 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  { k }  ->  ( i  / 
j )  =  ( i  /  k ) )
131130eleq1d 2512 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  { k }  ->  ( ( i  /  j )  e.  ( 0 [,] 1
)  <->  ( i  / 
k )  e.  ( 0 [,] 1 ) ) )
132128, 131syl5ibrcom 226 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  i  e.  ( 0 ... k ) )  ->  ( j  e. 
{ k }  ->  ( i  /  j )  e.  ( 0 [,] 1 ) ) )
133132impr 624 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  ( i  e.  ( 0 ... k )  /\  j  e.  {
k } ) )  ->  ( i  / 
j )  e.  ( 0 [,] 1 ) )
134101, 133sylan 474 . . . . . . . . . . . . . . . 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 765 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  p :
( 1 ... N
) --> ( 0 ... k ) )
136 vex 3047 . . . . . . . . . . . . . . . . . 18  |-  k  e. 
_V
137136fconst 5767 . . . . . . . . . . . . . . . . 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 12183 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  ( 1 ... N )  e. 
Fin )
140 inidm 3640 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
141134, 135, 138, 139, 139, 140off 6543 . . . . . . . . . . . . . . 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 2520 . . . . . . . . . . . . . . . 16  |-  ( ( p  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  I  <->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) )
144 ovex 6316 . . . . . . . . . . . . . . . . 17  |-  ( 0 [,] 1 )  e. 
_V
145 ovex 6316 . . . . . . . . . . . . . . . . 17  |-  ( 1 ... N )  e. 
_V
146144, 145elmap 7497 . . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . . 15  |-  ( ( p  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  I  <->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) : ( 1 ... N
) --> ( 0 [,] 1 ) )
148141, 147sylibr 216 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k ) ) )  ->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  I )
1491483adantr3 1168 . . . . . . . . . . . . 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 988 . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . . 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 5726 . . . . . . . . . . . . . . . . . 18  |-  ( p : ( 1 ... N ) --> ( 0 ... k )  ->  p  Fn  ( 1 ... N ) )
154153ad2antrl 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n )  =  k ) )  ->  p  Fn  ( 1 ... N
) )
155 fnconstg 5769 . . . . . . . . . . . . . . . . . 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 12183 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n )  =  k ) )  ->  (
1 ... N )  e. 
Fin )
158 simplrr 770 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  ( p : ( 1 ... N ) --> ( 0 ... k
)  /\  ( p `  n )  =  k ) )  /\  n  e.  ( 1 ... N
) )  ->  (
p `  n )  =  k )
159136fvconst2 6118 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
k } ) `  n )  =  k )
160159adantl 468 . . . . . . . . . . . . . . . . 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 6537 . . . . . . . . . . . . . . . 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 652 . . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . 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 10639 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  =/=  0 )
165118, 164dividd 10378 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  (
k  /  k )  =  1 )
166165ad2antlr 732 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( k  /  k )  =  1 )
167163, 166eqtrd 2484 . . . . . . . . . . . . 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 6316 . . . . . . . . . . . . . 14  |-  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e. 
_V
169 eleq1 2516 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
z  e.  I  <->  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  I ) )
170 fveq1 5862 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
z `  n )  =  ( ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) `  n ) )
171170eqeq1d 2452 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
( z `  n
)  =  1  <->  (
( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) `  n )  =  1 ) )
172169, 1713anbi23d 1341 . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . 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 5863 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  ( F `  z )  =  ( F `  ( p  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) )
175174fveq1d 5865 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
( F `  z
) `  n )  =  ( ( F `
 ( p  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) `  n ) )
176175breq2d 4413 . . . . . . . . . . . . . . 15  |-  ( z  =  ( p  oF  /  ( ( 1 ... N )  X.  { k } ) )  ->  (
0  <_  ( ( F `  z ) `  n )  <->  0  <_  ( ( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  n ) ) )
177173, 176imbi12d 322 . . . . . . . . . . . . . 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 3099 . . . . . . . . . . . . 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 1269 . . . . . . . . . . . 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 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
182 simp3 1009 . . . . . . . . . . . . 13  |-  ( ( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k )  ->  ( p `  n )  =  k )
183 neeq1 2685 . . . . . . . . . . . . . . 15  |-  ( ( p `  n )  =  k  ->  (
( p `  n
)  =/=  0  <->  k  =/=  0 ) )
184164, 183syl5ibrcom 226 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  (
( p `  n
)  =  k  -> 
( p `  n
)  =/=  0 ) )
185184imp 431 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  /\  ( p `  n
)  =  k )  ->  ( p `  n )  =/=  0
)
186181, 182, 185syl2an 480 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... k )  /\  ( p `  n
)  =  k ) )  ->  ( p `  n )  =/=  0
)
187 vex 3047 . . . . . . . . . . . . 13  |-  n  e. 
_V
188 fveq2 5863 . . . . . . . . . . . . . . 15  |-  ( b  =  n  ->  (
( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  b )  =  ( ( F `
 ( p  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) `  n ) )
189188breq2d 4413 . . . . . . . . . . . . . 14  |-  ( b  =  n  ->  (
0  <_  ( ( F `  ( p  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) `
 b )  <->  0  <_  ( ( F `  (
p  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) `  n ) ) )
19066neeq1d 2682 . . . . . . . . . . . . . 14  |-  ( b  =  n  ->  (
( p `  b
)  =/=  0  <->  (
p `  n )  =/=  0 ) )
191189, 190anbi12d 716 . . . . . . . . . . . . 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 4009 . . . . . . . . . . . 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 669 . . . . . . . . . . 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 11038 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  n  e.  CC )
195 1cnd 9656 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  1  e.  CC )
196194, 195subeq0ad 9993 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  =  0  <->  n  =  1 ) )
197196biimpcd 228 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  =  0  ->  (
n  e.  ( 1 ... N )  ->  n  =  1 ) )
198 1z 10964 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  ZZ
199 fzsn 11837 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
200198, 199ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... 1 )  =  { 1 }
201 oveq2 6296 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
1 ... n )  =  ( 1 ... 1
) )
202 sneq 3977 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  { n }  =  { 1 } )
203200, 201, 2023eqtr4a 2510 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
1 ... n )  =  { n } )
204203raleqdv 2992 . . . . . . . . . . . . . . . . . 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 227 . . . . . . . . . . . . . . . . 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 3615 . . . . . . . . . . . . . . . . . . . 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 10041 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  CC  ->  (
( n  -  1 )  +  1 )  =  n )
209194, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  +  1 )  =  n )
210 elfzuz 11793 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ( ZZ>= `  1 )
)
211209, 210eqeltrd 2528 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  (
( n  -  1 )  +  1 )  e.  ( ZZ>= `  1
) )
212 peano2zm 10977 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  ZZ  ->  (
n  -  1 )  e.  ZZ )
213 uzid 11170 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  -  1 )  e.  ZZ  ->  (
n  -  1 )  e.  ( ZZ>= `  (
n  -  1 ) ) )
214 peano2uz 11209 . . . . . . . . . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  n  e.  ( ZZ>= `  ( n  -  1 ) ) )
217 fzsplit2 11821 . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( 1 ... N )  ->  (
1 ... n )  =  ( ( 1 ... ( n  -  1 ) )  u.  (
( ( n  - 
1 )  +  1 ) ... n ) ) )
219209oveq1d 6303 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
( ( n  - 
1 )  +  1 ) ... n )  =  ( n ... n ) )
220 fzsn 11837 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  ZZ  ->  (
n ... n )  =  { n } )
22140, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( 1 ... N )  ->  (
n ... n )  =  { n } )
222219, 221eqtrd 2484 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... N )  ->  (
( ( n  - 
1 )  +  1 ) ... n )  =  { n }
)
223222uneq2d 3587 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( 1 ... N )  ->  (
( 1 ... (
n  -  1 ) )  u.  ( ( ( n  -  1 )  +  1 ) ... n ) )  =  ( ( 1 ... ( n  - 
1 ) )  u. 
{ n } ) )
224218, 223eqtrd 2484 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... N )  ->  (
1 ... n )  =  ( ( 1 ... ( n  -  1 ) )  u.  {
n } ) )
225224raleqdv 2992 . . . . . . . . . . . . . . . . . . . 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 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
) ) )
227226expd 438 . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . 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 381 . . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . . 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 3573 . . . . . . . . . . . . . 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 6316 . . . . . . . . . . . . . . . 16  |-  ( n  -  1 )  e. 
_V
235234elsnc 3991 . . . . . . . . . . . . . . 15  |-  ( ( n  -  1 )  e.  { 0 }  <-> 
( n  -  1 )  =  0 )
236 oveq2 6296 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( n  - 
1 )  ->  (
1 ... a )  =  ( 1 ... (
n  -  1 ) ) )
237236raleqdv 2992 . . . . . . . . . . . . . . . 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 3195 . . . . . . . . . . . . . . 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 524 . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . 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 6296 . . . . . . . . . . . . . . 15  |-  ( a  =  n  ->  (
1 ... a )  =  ( 1 ... n
) )
242241raleqdv 2992 . . . . . . . . . . . . . 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 3195 . . . . . . . . . . . . 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 274 . . . . . . . . . . . 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 3601 . . . . . . . . . . . 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 666 . . . . . . . . . 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 10549 . . . . . . . . . . . . 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 677 . . . . . . . . . . . 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 1185 . . . . . . . . . . 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 10579 . . . . . . . . . 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 10442 . . . . . . . . . 10  |-  ( n  e.  RR  ->  (
n  -  1 )  <  n )
254 peano2rem 9938 . . . . . . . . . . 11  |-  ( n  e.  RR  ->  (
n  -  1 )  e.  RR )
25545, 48sselii 3428 . . . . . . . . . . . 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 9722 . . . . . . . . . . . 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 1352 . . . . . . . . . . 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 )