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

Theorem poimir 31881
Description: Poincare-Miranda theorem. Theorem on [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
poimir  |-  ( ph  ->  E. c  e.  I 
( F `  c
)  =  ( ( 1 ... N )  X.  { 0 } ) )
Distinct variable groups:    z, n, ph    n, F    n, N    ph, z    z, F    z, N    n, c, z, ph    F, c    I,
c, n, z    N, c    R, c, n, z

Proof of Theorem poimir
Dummy variables  x  r  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poimir.0 . . 3  |-  ( ph  ->  N  e.  NN )
2 poimir.i . . 3  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
3 poimir.r . . 3  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
4 poimir.1 . . 3  |-  ( ph  ->  F  e.  ( ( Rt  I )  Cn  R
) )
5 poimir.2 . . 3  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  z  e.  I  /\  ( z `  n )  =  0 ) )  ->  (
( F `  z
) `  n )  <_  0 )
6 poimir.3 . . 3  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  z  e.  I  /\  ( z `  n )  =  1 ) )  ->  0  <_  ( ( F `  z ) `  n
) )
71, 2, 3, 4, 5, 6poimirlem32 31880 . 2  |-  ( 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 )
) )
8 ovex 6325 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1 ... N )  e. 
_V
9 retopon 21761 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  (TopOn `  RR )
103pttoponconst 20589 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 1 ... N
)  e.  _V  /\  ( topGen `  ran  (,) )  e.  (TopOn `  RR )
)  ->  R  e.  (TopOn `  ( RR  ^m  ( 1 ... N
) ) ) )
118, 9, 10mp2an 676 . . . . . . . . . . . . . . . . . . . . 21  |-  R  e.  (TopOn `  ( RR  ^m  ( 1 ... N
) ) )
1211topontopi 19923 . . . . . . . . . . . . . . . . . . . 20  |-  R  e. 
Top
13 reex 9626 . . . . . . . . . . . . . . . . . . . . . 22  |-  RR  e.  _V
14 unitssre 11773 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 [,] 1 )  C_  RR
15 mapss 7514 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  e.  _V  /\  ( 0 [,] 1
)  C_  RR )  ->  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) 
C_  ( RR  ^m  ( 1 ... N
) ) )
1613, 14, 15mp2an 676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  C_  ( RR  ^m  (
1 ... N ) )
172, 16eqsstri 3491 . . . . . . . . . . . . . . . . . . . 20  |-  I  C_  ( RR  ^m  (
1 ... N ) )
1811toponunii 19924 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
^m  ( 1 ... N ) )  = 
U. R
1918restuni 20155 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  Top  /\  I  C_  ( RR  ^m  ( 1 ... N
) ) )  ->  I  =  U. ( Rt  I ) )
2012, 17, 19mp2an 676 . . . . . . . . . . . . . . . . . . 19  |-  I  = 
U. ( Rt  I )
2120, 18cnf 20239 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  ( ( Rt  I )  Cn  R )  ->  F : I --> ( RR  ^m  (
1 ... N ) ) )
224, 21syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F : I --> ( RR 
^m  ( 1 ... N ) ) )
2322ffvelrnda 6029 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  I )  ->  ( F `  c )  e.  ( RR  ^m  (
1 ... N ) ) )
24 elmapi 7493 . . . . . . . . . . . . . . . 16  |-  ( ( F `  c )  e.  ( RR  ^m  ( 1 ... N
) )  ->  ( F `  c ) : ( 1 ... N ) --> RR )
2523, 24syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  I )  ->  ( F `  c ) : ( 1 ... N ) --> RR )
2625ffvelrnda 6029 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( F `  c
) `  n )  e.  RR )
27 recn 9625 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( ( F `  c ) `  n )  e.  CC )
28 absrpcl 13330 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  CC  /\  ( ( F `  c ) `  n
)  =/=  0 )  ->  ( abs `  (
( F `  c
) `  n )
)  e.  RR+ )
2928ex 435 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  CC  ->  ( (
( F `  c
) `  n )  =/=  0  ->  ( abs `  ( ( F `  c ) `  n
) )  e.  RR+ ) )
3027, 29syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  =/=  0  ->  ( abs `  ( ( F `  c ) `  n
) )  e.  RR+ ) )
31 ltsubrp 11331 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR+ )  ->  (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  < 
( ( F `  c ) `  n
) )
32 ltaddrp 11332 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR+ )  ->  (
( F `  c
) `  n )  <  ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )
3331, 32jca 534 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR+ )  ->  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  <  ( ( F `
 c ) `  n )  /\  (
( F `  c
) `  n )  <  ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )
3433ex 435 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( ( abs `  ( ( F `
 c ) `  n ) )  e.  RR+  ->  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  <  (
( F `  c
) `  n )  /\  ( ( F `  c ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
3530, 34syld 45 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  =/=  0  ->  ( ( ( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  < 
( ( F `  c ) `  n
)  /\  ( ( F `  c ) `  n )  <  (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) ) ) )
3627abscld 13476 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( abs `  ( ( F `  c ) `  n
) )  e.  RR )
37 resubcl 9934 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  e.  RR )
3836, 37mpdan 672 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  e.  RR )
3938rexrd 9686 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  e.  RR* )
40 readdcl 9618 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR )  -> 
( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) )  e.  RR )
4136, 40mpdan 672 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  e.  RR )
4241rexrd 9686 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  e.  RR* )
43 rexr 9682 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( ( F `  c ) `  n )  e.  RR* )
44 elioo5 11688 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  e.  RR*  /\  (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) )  e. 
RR*  /\  ( ( F `  c ) `  n )  e.  RR* )  ->  ( ( ( F `  c ) `
 n )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  <->  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  < 
( ( F `  c ) `  n
)  /\  ( ( F `  c ) `  n )  <  (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) ) ) )
4539, 42, 43, 44syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  <->  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  < 
( ( F `  c ) `  n
)  /\  ( ( F `  c ) `  n )  <  (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) ) ) )
4635, 45sylibrd 237 . . . . . . . . . . . . . 14  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  =/=  0  ->  ( ( F `  c ) `
 n )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
4726, 46syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  =/=  0  -> 
( ( F `  c ) `  n
)  e.  ( ( ( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) ) )
48 fveq2 5873 . . . . . . . . . . . . . . . . 17  |-  ( x  =  c  ->  ( F `  x )  =  ( F `  c ) )
4948fveq1d 5875 . . . . . . . . . . . . . . . 16  |-  ( x  =  c  ->  (
( F `  x
) `  n )  =  ( ( F `
 c ) `  n ) )
50 eqid 2420 . . . . . . . . . . . . . . . 16  |-  ( x  e.  I  |->  ( ( F `  x ) `
 n ) )  =  ( x  e.  I  |->  ( ( F `
 x ) `  n ) )
51 fvex 5883 . . . . . . . . . . . . . . . 16  |-  ( ( F `  c ) `
 n )  e. 
_V
5249, 50, 51fvmpt 5956 . . . . . . . . . . . . . . 15  |-  ( c  e.  I  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  c
)  =  ( ( F `  c ) `
 n ) )
5352eleq1d 2489 . . . . . . . . . . . . . 14  |-  ( c  e.  I  ->  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) `  c )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  <->  ( ( F `  c ) `  n )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
5453ad2antlr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) `  c )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  <->  ( ( F `  c ) `  n )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
5547, 54sylibrd 237 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  =/=  0  -> 
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) `  c )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
56 iooretop 21763 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )  e.  (
topGen `  ran  (,) )
57 resttopon 20154 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  (TopOn `  ( RR  ^m  (
1 ... N ) ) )  /\  I  C_  ( RR  ^m  (
1 ... N ) ) )  ->  ( Rt  I
)  e.  (TopOn `  I ) )
5811, 17, 57mp2an 676 . . . . . . . . . . . . . . . . . . 19  |-  ( Rt  I )  e.  (TopOn `  I )
5958a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( Rt  I )  e.  (TopOn `  I ) )
6022feqmptd 5926 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  =  ( x  e.  I  |->  ( F `
 x ) ) )
6160, 4eqeltrrd 2509 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  I  |->  ( F `  x
) )  e.  ( ( Rt  I )  Cn  R
) )
6261adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  I  |->  ( F `  x ) )  e.  ( ( Rt  I )  Cn  R
) )
6311a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  R  e.  (TopOn `  ( RR  ^m  ( 1 ... N
) ) ) )
64 retop 21759 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
6564fconst6 5782 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Top
6618, 3ptpjcn 20603 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1 ... N
)  e.  _V  /\  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) --> Top  /\  n  e.  ( 1 ... N
) )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) ) )
678, 65, 66mp3an12 1350 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) ) )
68 fvex 5883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  _V
6968fvconst2 6127 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  =  ( topGen ` 
ran  (,) ) )
7069oveq2d 6313 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  ( R  Cn  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  =  ( R  Cn  ( topGen `  ran  (,) )
) )
7167, 70eleqtrd 2510 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( topGen `  ran  (,) ) ) )
7271adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( topGen `  ran  (,) ) ) )
73 fveq1 5872 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( F `  x )  ->  (
z `  n )  =  ( ( F `
 x ) `  n ) )
7459, 62, 63, 72, 73cnmpt11 20655 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( Rt  I )  Cn  ( topGen `
 ran  (,) )
) )
7520cncnpi 20271 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  e.  I  |->  ( ( F `  x ) `  n
) )  e.  ( ( Rt  I )  Cn  ( topGen `
 ran  (,) )
)  /\  c  e.  I )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( ( Rt  I )  CnP  ( topGen `
 ran  (,) )
) `  c )
)
7674, 75sylan 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  c  e.  I )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( ( Rt  I )  CnP  ( topGen `
 ran  (,) )
) `  c )
)
7776an32s 811 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( ( Rt  I )  CnP  ( topGen `
 ran  (,) )
) `  c )
)
78 iscnp 20230 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Rt  I )  e.  (TopOn `  I )  /\  ( topGen `
 ran  (,) )  e.  (TopOn `  RR )  /\  c  e.  I
)  ->  ( (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( ( Rt  I )  CnP  ( topGen `
 ran  (,) )
) `  c )  <->  ( ( x  e.  I  |->  ( ( F `  x ) `  n
) ) : I --> RR  /\  A. z  e.  ( topGen `  ran  (,) )
( ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) `
 c )  e.  z  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )
) ) ) )
7958, 9, 78mp3an12 1350 . . . . . . . . . . . . . . . 16  |-  ( c  e.  I  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) )  e.  ( ( ( Rt  I )  CnP  ( topGen `  ran  (,) ) ) `  c
)  <->  ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) : I --> RR  /\  A. z  e.  ( topGen ` 
ran  (,) ) ( ( ( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  c
)  e.  z  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )
) ) ) )
8079ad2antlr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) )  e.  ( ( ( Rt  I )  CnP  ( topGen `  ran  (,) ) ) `  c
)  <->  ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) : I --> RR  /\  A. z  e.  ( topGen ` 
ran  (,) ) ( ( ( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  c
)  e.  z  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )
) ) ) )
8177, 80mpbid 213 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) : I --> RR  /\  A. z  e.  ( topGen `  ran  (,) )
( ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) `
 c )  e.  z  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )
) ) )
8281simprd 464 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  A. z  e.  ( topGen `  ran  (,) )
( ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) `
 c )  e.  z  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )
) )
83 eleq2 2493 . . . . . . . . . . . . . . 15  |-  ( z  =  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) )  ->  ( ( ( x  e.  I  |->  ( ( F `  x
) `  n )
) `  c )  e.  z  <->  ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) `
 c )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
84 sseq2 3483 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) )  ->  ( ( ( x  e.  I  |->  ( ( F `  x
) `  n )
) " v ) 
C_  z  <->  ( (
x  e.  I  |->  ( ( F `  x
) `  n )
) " v ) 
C_  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) ) ) )
8584anbi2d 708 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) )  ->  ( ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )  <->  ( c  e.  v  /\  ( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) ) )
8685rexbidv 2937 . . . . . . . . . . . . . . 15  |-  ( z  =  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) )  ->  ( E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )  <->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  ( ( x  e.  I  |->  ( ( F `  x
) `  n )
) " v ) 
C_  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) ) ) ) )
8783, 86imbi12d 321 . . . . . . . . . . . . . 14  |-  ( z  =  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) )  ->  ( ( ( ( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  c
)  e.  z  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )
)  <->  ( ( ( x  e.  I  |->  ( ( F `  x
) `  n )
) `  c )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) ) ) ) )
8887rspcv 3175 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  e.  ( topGen `  ran  (,) )  ->  ( A. z  e.  ( topGen `  ran  (,) )
( ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) `
 c )  e.  z  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  z )
)  ->  ( (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  c
)  e.  ( ( ( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) ) ) ) )
8956, 82, 88mpsyl 65 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) `  c )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) ) ) )
9055, 89syld 45 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  =/=  0  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) ) ) )
91 0re 9639 . . . . . . . . . . . 12  |-  0  e.  RR
92 letric 9730 . . . . . . . . . . . 12  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  e.  RR )  ->  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) )
9326, 91, 92sylancl 666 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  <_  0  \/  0  <_  ( ( F `
 c ) `  n ) ) )
9490, 93jctird 546 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  =/=  0  -> 
( E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) ) ) )
95 r19.41v 2978 . . . . . . . . . . 11  |-  ( E. v  e.  ( Rt  I ) ( ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) )  <->  ( E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) ) )
96 anass 653 . . . . . . . . . . . 12  |-  ( ( ( c  e.  v  /\  ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) )
" v )  C_  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) )  /\  ( ( ( F `  c ) `
 n )  <_ 
0  \/  0  <_ 
( ( F `  c ) `  n
) ) )  <->  ( c  e.  v  /\  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) ) ) )
9796rexbii 2925 . . . . . . . . . . 11  |-  ( E. v  e.  ( Rt  I ) ( ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) )  <->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) ) ) )
9895, 97bitr3i 254 . . . . . . . . . 10  |-  ( ( E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) )  <->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) ) ) )
9994, 98syl6ib 229 . . . . . . . . 9  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  =/=  0  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) ) ) ) )
10058topontopi 19923 . . . . . . . . . . . . 13  |-  ( Rt  I )  e.  Top
10120eltopss 19914 . . . . . . . . . . . . 13  |-  ( ( ( Rt  I )  e.  Top  /\  v  e.  ( Rt  I ) )  ->  v  C_  I )
102100, 101mpan 674 . . . . . . . . . . . 12  |-  ( v  e.  ( Rt  I )  ->  v  C_  I
)
103 fvex 5883 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  x ) `
 n )  e. 
_V
104103, 50dmmpti 5717 . . . . . . . . . . . . . . . . 17  |-  dom  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  =  I
105104sseq2i 3486 . . . . . . . . . . . . . . . 16  |-  ( v 
C_  dom  ( x  e.  I  |->  ( ( F `  x ) `
 n ) )  <-> 
v  C_  I )
106 funmpt 5629 . . . . . . . . . . . . . . . . 17  |-  Fun  (
x  e.  I  |->  ( ( F `  x
) `  n )
)
107 funimass4 5924 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  ( x  e.  I  |->  ( ( F `
 x ) `  n ) )  /\  v  C_  dom  ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) )  ->  ( (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )  <->  A. z  e.  v  ( (
x  e.  I  |->  ( ( F `  x
) `  n )
) `  z )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
108106, 107mpan 674 . . . . . . . . . . . . . . . 16  |-  ( v 
C_  dom  ( x  e.  I  |->  ( ( F `  x ) `
 n ) )  ->  ( ( ( x  e.  I  |->  ( ( F `  x
) `  n )
) " v ) 
C_  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) )  <->  A. z  e.  v 
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) `  z )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
109105, 108sylbir 216 . . . . . . . . . . . . . . 15  |-  ( v 
C_  I  ->  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  <->  A. z  e.  v  ( (
x  e.  I  |->  ( ( F `  x
) `  n )
) `  z )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
110 ssel2 3456 . . . . . . . . . . . . . . . . 17  |-  ( ( v  C_  I  /\  z  e.  v )  ->  z  e.  I )
111 fveq2 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
112111fveq1d 5875 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
( F `  x
) `  n )  =  ( ( F `
 z ) `  n ) )
113 fvex 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  z ) `
 n )  e. 
_V
114112, 50, 113fvmpt 5956 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  I  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  z
)  =  ( ( F `  z ) `
 n ) )
115114eleq1d 2489 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  I  ->  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) `  z )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  <->  ( ( F `  z ) `  n )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
116 eliooord 11690 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  z
) `  n )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  -> 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) )
117115, 116syl6bi 231 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  I  ->  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) `  z )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  -> 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
118110, 117syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( v  C_  I  /\  z  e.  v )  ->  ( ( ( x  e.  I  |->  ( ( F `  x ) `
 n ) ) `
 z )  e.  ( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) ) (,) ( ( ( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  -> 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
119118ralimdva 2831 . . . . . . . . . . . . . . 15  |-  ( v 
C_  I  ->  ( A. z  e.  v 
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) `  z )  e.  ( ( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  A. z  e.  v 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
120109, 119sylbid 218 . . . . . . . . . . . . . 14  |-  ( v 
C_  I  ->  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  A. z  e.  v 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) ) ) )
121120adantl 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  v  C_  I
)  ->  ( (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )  ->  A. z  e.  v  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  < 
( ( F `  z ) `  n
)  /\  ( ( F `  z ) `  n )  <  (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) ) ) )
122 absnid 13340 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( abs `  (
( F `  c
) `  n )
)  =  -u (
( F `  c
) `  n )
)
123122oveq2d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) )  =  ( ( ( F `  c ) `  n
)  +  -u (
( F `  c
) `  n )
) )
12427negidd 9972 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  -u ( ( F `
 c ) `  n ) )  =  0 )
125124adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( ( ( F `  c ) `
 n )  + 
-u ( ( F `
 c ) `  n ) )  =  0 )
126123, 125eqtrd 2461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
12726, 126sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  ( ( F `
 c ) `  n )  <_  0
)  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
128127adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  ( ( F `  c ) `
 n )  <_ 
0 )  /\  z  e.  I )  ->  (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) )  =  0 )
129128breq2d 4429 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  ( ( F `  c ) `
 n )  <_ 
0 )  /\  z  e.  I )  ->  (
( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  <->  ( ( F `  z ) `  n )  <  0
) )
13022ffvelrnda 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  I )  ->  ( F `  z )  e.  ( RR  ^m  (
1 ... N ) ) )
131 elmapi 7493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  z )  e.  ( RR  ^m  ( 1 ... N
) )  ->  ( F `  z ) : ( 1 ... N ) --> RR )
132130, 131syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  I )  ->  ( F `  z ) : ( 1 ... N ) --> RR )
133132ffvelrnda 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( F `  z
) `  n )  e.  RR )
134133an32s 811 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
( F `  z
) `  n )  e.  RR )
135 0red 9640 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  0  e.  RR )
136134, 135ltnled 9778 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
( ( F `  z ) `  n
)  <  0  <->  -.  0  <_  ( ( F `  z ) `  n
) ) )
137136adantllr 723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  z  e.  I
)  ->  ( (
( F `  z
) `  n )  <  0  <->  -.  0  <_  ( ( F `  z
) `  n )
) )
138137adantlr 719 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  ( ( F `  c ) `
 n )  <_ 
0 )  /\  z  e.  I )  ->  (
( ( F `  z ) `  n
)  <  0  <->  -.  0  <_  ( ( F `  z ) `  n
) ) )
139129, 138bitrd 256 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  ( ( F `  c ) `
 n )  <_ 
0 )  /\  z  e.  I )  ->  (
( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  <->  -.  0  <_  ( ( F `  z ) `  n
) ) )
140139biimpd 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  ( ( F `  c ) `
 n )  <_ 
0 )  /\  z  e.  I )  ->  (
( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  ->  -.  0  <_  ( ( F `
 z ) `  n ) ) )
141110, 140sylan2 476 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  ( ( F `  c ) `
 n )  <_ 
0 )  /\  (
v  C_  I  /\  z  e.  v )
)  ->  ( (
( F `  z
) `  n )  <  ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) )  ->  -.  0  <_  ( ( F `  z ) `  n
) ) )
142141anassrs 652 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  /\  (
( F `  c
) `  n )  <_  0 )  /\  v  C_  I )  /\  z  e.  v )  ->  (
( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  ->  -.  0  <_  ( ( F `
 z ) `  n ) ) )
143142adantld 468 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  /\  (
( F `  c
) `  n )  <_  0 )  /\  v  C_  I )  /\  z  e.  v )  ->  (
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  -.  0  <_  ( ( F `  z ) `
 n ) ) )
144143ralimdva 2831 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  ( ( F `  c ) `
 n )  <_ 
0 )  /\  v  C_  I )  ->  ( A. z  e.  v 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  A. z  e.  v  -.  0  <_  ( ( F `  z ) `
 n ) ) )
145144an32s 811 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  v  C_  I )  /\  (
( F `  c
) `  n )  <_  0 )  ->  ( A. z  e.  v 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  A. z  e.  v  -.  0  <_  ( ( F `  z ) `
 n ) ) )
146145impancom 441 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  v  C_  I )  /\  A. z  e.  v  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  <  ( ( F `
 z ) `  n )  /\  (
( F `  z
) `  n )  <  ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )  -> 
( ( ( F `
 c ) `  n )  <_  0  ->  A. z  e.  v  -.  0  <_  (
( F `  z
) `  n )
) )
147 absid 13338 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( abs `  (
( F `  c
) `  n )
)  =  ( ( F `  c ) `
 n ) )
148147oveq2d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  =  ( ( ( F `  c ) `
 n )  -  ( ( F `  c ) `  n
) ) )
14927subidd 9970 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( ( F `
 c ) `  n ) )  =  0 )
150149adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  (
( F `  c
) `  n )
)  =  0 )
151148, 150eqtrd 2461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  =  0 )
15226, 151sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  0  <_  (
( F `  c
) `  n )
)  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
153152adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  0  <_ 
( ( F `  c ) `  n
) )  /\  z  e.  I )  ->  (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  =  0 )
154153breq1d 4427 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  0  <_ 
( ( F `  c ) `  n
) )  /\  z  e.  I )  ->  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  <  ( ( F `
 z ) `  n )  <->  0  <  ( ( F `  z
) `  n )
) )
155135, 134ltnled 9778 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
0  <  ( ( F `  z ) `  n )  <->  -.  (
( F `  z
) `  n )  <_  0 ) )
156155adantllr 723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  z  e.  I
)  ->  ( 0  <  ( ( F `
 z ) `  n )  <->  -.  (
( F `  z
) `  n )  <_  0 ) )
157156adantlr 719 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  0  <_ 
( ( F `  c ) `  n
) )  /\  z  e.  I )  ->  (
0  <  ( ( F `  z ) `  n )  <->  -.  (
( F `  z
) `  n )  <_  0 ) )
158154, 157bitrd 256 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  0  <_ 
( ( F `  c ) `  n
) )  /\  z  e.  I )  ->  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  <  ( ( F `
 z ) `  n )  <->  -.  (
( F `  z
) `  n )  <_  0 ) )
159158biimpd 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  0  <_ 
( ( F `  c ) `  n
) )  /\  z  e.  I )  ->  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  <  ( ( F `
 z ) `  n )  ->  -.  ( ( F `  z ) `  n
)  <_  0 ) )
160110, 159sylan2 476 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  0  <_ 
( ( F `  c ) `  n
) )  /\  (
v  C_  I  /\  z  e.  v )
)  ->  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  < 
( ( F `  z ) `  n
)  ->  -.  (
( F `  z
) `  n )  <_  0 ) )
161160anassrs 652 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  /\  0  <_  ( ( F `  c ) `  n
) )  /\  v  C_  I )  /\  z  e.  v )  ->  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  <  ( ( F `
 z ) `  n )  ->  -.  ( ( F `  z ) `  n
)  <_  0 ) )
162161adantrd 469 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  /\  0  <_  ( ( F `  c ) `  n
) )  /\  v  C_  I )  /\  z  e.  v )  ->  (
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  -.  ( ( F `  z ) `  n
)  <_  0 ) )
163162ralimdva 2831 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  0  <_ 
( ( F `  c ) `  n
) )  /\  v  C_  I )  ->  ( A. z  e.  v 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) )
164163an32s 811 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  v  C_  I )  /\  0  <_  ( ( F `  c ) `  n
) )  ->  ( A. z  e.  v 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  ->  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) )
165164impancom 441 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  v  C_  I )  /\  A. z  e.  v  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  <  ( ( F `
 z ) `  n )  /\  (
( F `  z
) `  n )  <  ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )  -> 
( 0  <_  (
( F `  c
) `  n )  ->  A. z  e.  v  -.  ( ( F `
 z ) `  n )  <_  0
) )
166146, 165orim12d 846 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N ) )  /\  v  C_  I )  /\  A. z  e.  v  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  <  ( ( F `
 z ) `  n )  /\  (
( F `  z
) `  n )  <  ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) ) )  -> 
( ( ( ( F `  c ) `
 n )  <_ 
0  \/  0  <_ 
( ( F `  c ) `  n
) )  ->  ( A. z  e.  v  -.  0  <_  ( ( F `  z ) `
 n )  \/ 
A. z  e.  v  -.  ( ( F `
 z ) `  n )  <_  0
) ) )
167166expimpd 606 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  v  C_  I
)  ->  ( ( A. z  e.  v 
( ( ( ( F `  c ) `
 n )  -  ( abs `  ( ( F `  c ) `
 n ) ) )  <  ( ( F `  z ) `
 n )  /\  ( ( F `  z ) `  n
)  <  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) )  ->  ( A. z  e.  v  -.  0  <_  ( ( F `
 z ) `  n )  \/  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) ) )
168121, 167syland 483 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  v  C_  I
)  ->  ( (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) )  ->  ( A. z  e.  v  -.  0  <_  ( ( F `
 z ) `  n )  \/  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) ) )
169102, 168sylan2 476 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  v  e.  ( Rt  I ) )  -> 
( ( ( ( x  e.  I  |->  ( ( F `  x
) `  n )
) " v ) 
C_  ( ( ( ( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) ) (,) (
( ( F `  c ) `  n
)  +  ( abs `  ( ( F `  c ) `  n
) ) ) )  /\  ( ( ( F `  c ) `
 n )  <_ 
0  \/  0  <_ 
( ( F `  c ) `  n
) ) )  -> 
( A. z  e.  v  -.  0  <_ 
( ( F `  z ) `  n
)  \/  A. z  e.  v  -.  (
( F `  z
) `  n )  <_  0 ) ) )
170169anim2d 567 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  v  e.  ( Rt  I ) )  -> 
( ( c  e.  v  /\  ( ( ( x  e.  I  |->  ( ( F `  x ) `  n
) ) " v
)  C_  ( (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )  /\  (
( ( F `  c ) `  n
)  <_  0  \/  0  <_  ( ( F `
 c ) `  n ) ) ) )  ->  ( c  e.  v  /\  ( A. z  e.  v  -.  0  <_  ( ( F `  z ) `
 n )  \/ 
A. z  e.  v  -.  ( ( F `
 z ) `  n )  <_  0
) ) ) )
171170reximdva 2898 . . . . . . . . 9  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  ( E. v  e.  ( Rt  I ) ( c  e.  v  /\  (
( ( x  e.  I  |->  ( ( F `
 x ) `  n ) ) "
v )  C_  (
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) ) (,) ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) ) )  /\  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) ) )  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  ( A. z  e.  v  -.  0  <_  ( ( F `  z ) `
 n )  \/ 
A. z  e.  v  -.  ( ( F `
 z ) `  n )  <_  0
) ) ) )
17299, 171syld 45 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  =/=  0  ->  E. v  e.  ( Rt  I ) ( c  e.  v  /\  ( A. z  e.  v  -.  0  <_  ( ( F `  z ) `
 n )  \/ 
A. z  e.  v  -.  ( ( F `
 z ) `  n )  <_  0
) ) ) )
173 ralnex 2869 . . . . . . . . . . . . . 14  |-  ( A. z  e.  v  -.  0 r ( ( F `  z ) `
 n )  <->  -.  E. z  e.  v  0 r ( ( F `  z ) `  n
) )
174173rexbii 2925 . . . . . . . . . . . . 13  |-  ( E. r  e.  {  <_  ,  `'  <_  } A. z  e.  v  -.  0
r ( ( F `
 z ) `  n )  <->  E. r  e.  {  <_  ,  `'  <_  }  -.  E. z  e.  v  0 r ( ( F `  z ) `  n
) )
175 letsr 16451 . . . . . . . . . . . . . . 15  |-  <_  e.  TosetRel
176175elexi 3088 . . . . . . . . . . . . . 14  |-  <_  e.  _V
177176cnvex 6746 . . . . . . . . . . . . . 14  |-  `'  <_  e. 
_V
178 breq 4419 . . . . . . . . . . . . . . . 16  |-  ( r  =  <_  ->  ( 0 r ( ( F `
 z ) `  n )  <->  0  <_  ( ( F `  z
) `  n )
) )
179178notbid 295 . . . . . . . . . . . . . . 15  |-  ( r  =  <_  ->  ( -.  0 r ( ( F `  z ) `
 n )  <->  -.  0  <_  ( ( F `  z ) `  n
) ) )
180179ralbidv 2862 . . . . . . . . . . . . . 14  |-  ( r  =  <_  ->  ( A. z  e.  v  -.  0 r ( ( F `  z ) `
 n )  <->  A. z  e.  v  -.  0  <_  ( ( F `  z ) `  n
) ) )
181 breq 4419 . . . . . . . . . . . . . . . . 17  |-  ( r  =  `'  <_  ->  ( 0 r ( ( F `  z ) `
 n )  <->  0 `'  <_  ( ( F `  z ) `  n
) ) )
182 c0ex 9633 . . . . . . . . . . . . . . . . . 18  |-  0  e.  _V
183182, 113brcnv 5029 . . . . . . . . . . . . . . . . 17  |-  ( 0 `'  <_  ( ( F `
 z ) `  n )  <->  ( ( F `  z ) `  n )  <_  0
)
184181, 183syl6bb 264 . . . . . . . . . . . . . . . 16  |-  ( r  =  `'  <_  ->  ( 0 r ( ( F `  z ) `
 n )  <->  ( ( F `  z ) `  n )  <_  0
) )
185184notbid 295 . . . . . . . . . . . . . . 15  |-  ( r  =  `'  <_  ->  ( -.  0 r ( ( F `  z
) `  n )  <->  -.  ( ( F `  z ) `  n
)  <_  0 ) )
186185ralbidv 2862 . . . . . . . . . . . . . 14  |-  ( r  =  `'  <_  ->  ( A. z  e.  v  -.  0 r ( ( F `  z
) `  n )  <->  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) )
187176, 177, 180, 186rexpr 4048 . . . . . . . . . . . . 13  |-  ( E. r  e.  {  <_  ,  `'  <_  } A. z  e.  v  -.  0
r ( ( F `
 z ) `  n )  <->  ( A. z  e.  v  -.  0  <_  ( ( F `
 z ) `  n )  \/  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) )
188 rexnal 2871 . . . . . . . . . . . . 13  |-  ( E. r  e.  {  <_  ,  `'  <_  }  -.  E. z  e.  v  0
r ( ( F `
 z ) `  n )  <->  -.  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
)
189174, 187, 1883bitr3i 278 . . . . . . . . . . . 12  |-  ( ( A. z  e.  v  -.  0  <_  (
( F `  z
) `  n )  \/  A. z  e.  v  -.  ( ( F `
 z ) `  n )  <_  0
)  <->  -.  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
)
190189anbi2i 698 . . . . . . . . . . 11  |-  ( ( c  e.  v  /\  ( A. z  e.  v  -.  0  <_  (
( F `  z
) `  n )  \/  A. z  e.  v  -.  ( ( F `
 z ) `  n )  <_  0
) )  <->  ( c  e.  v  /\  -.  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z ) `  n
) ) )
191 annim 426 . . . . . . . . . . 11  |-  ( ( c  e.  v  /\  -.  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0
r ( ( F `
 z ) `  n ) )  <->  -.  (
c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z ) `  n
) ) )
192190, 191bitri 252 . . . . . . . . . 10  |-  ( ( c  e.  v  /\  ( A. z  e.  v  -.  0  <_  (
( F `  z
) `  n )  \/  A. z  e.  v  -.  ( ( F `
 z ) `  n )  <_  0
) )  <->  -.  (
c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z ) `  n
) ) )
193192rexbii 2925 . . . . . . . . 9  |-  ( E. v  e.  ( Rt  I ) ( c  e.  v  /\  ( A. z  e.  v  -.  0  <_  ( ( F `
 z ) `  n )  \/  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) )  <->  E. v  e.  ( Rt  I )  -.  (
c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z ) `  n
) ) )
194 rexnal 2871 . . . . . . . . 9  |-  ( E. v  e.  ( Rt  I )  -.  ( c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
)  <->  -.  A. v  e.  ( Rt  I ) ( c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
) )
195193, 194bitri 252 . . . . . . . 8  |-  ( E. v  e.  ( Rt  I ) ( c  e.  v  /\  ( A. z  e.  v  -.  0  <_  ( ( F `
 z ) `  n )  \/  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) )  <->  -.  A. v  e.  ( Rt  I ) ( c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
) )
196172, 195syl6ib 229 . . . . . . 7  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  =/=  0  ->  -.  A. v  e.  ( Rt  I ) ( c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
) ) )
197196necon4ad 2642 . . . . . 6  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  ( A. v  e.  ( Rt  I ) ( c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
)  ->  ( ( F `  c ) `  n )  =  0 ) )
198197ralimdva 2831 . . . . 5  |-  ( (
ph  /\  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 )
)  ->  A. n  e.  ( 1 ... N
) ( ( F `
 c ) `  n )  =  0 ) )
199 ffn 5738 . . . . . 6  |-  ( ( F `  c ) : ( 1 ... N ) --> RR  ->  ( F `  c )  Fn  ( 1 ... N ) )
20025, 199syl 17 . . . . 5  |-  ( (
ph  /\  c  e.  I )  ->  ( F `  c )  Fn  ( 1 ... N
) )
201198, 200jctild 545 . . . 4  |-  ( (
ph  /\  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 )
)  ->  ( ( F `  c )  Fn  ( 1 ... N
)  /\  A. n  e.  ( 1 ... N
) ( ( F `
 c ) `  n )  =  0 ) ) )
202 fconstfv 6133 . . . . 5  |-  ( ( F `  c ) : ( 1 ... N ) --> { 0 }  <->  ( ( F `
 c )  Fn  ( 1 ... N
)  /\  A. n  e.  ( 1 ... N
) ( ( F `
 c ) `  n )  =  0 ) )
203182fconst2 6128 . . . . 5  |-  ( ( F `  c ) : ( 1 ... N ) --> { 0 }  <->  ( F `  c )  =  ( ( 1 ... N
)  X.  { 0 } ) )
204202, 203bitr3i 254 . . . 4  |-  ( ( ( F `  c
)  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( ( F `  c
) `  n )  =  0 )  <->  ( F `  c )  =  ( ( 1 ... N
)  X.  { 0 } ) )
205201, 204syl6ib 229 . . 3  |-  ( (
ph  /\  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 )
)  ->  ( F `  c )  =  ( ( 1 ... N
)  X.  { 0 } ) ) )
206205reximdva 2898 . 2  |-  ( 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 )
)  ->  E. c  e.  I  ( F `  c )  =  ( ( 1 ... N
)  X.  { 0 } ) ) )
2077, 206mpd 15 1  |-  ( ph  ->  E. c  e.  I 
( F `  c
)  =  ( ( 1 ... N )  X.  { 0 } ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1867    =/= wne 2616   A.wral 2773   E.wrex 2774   _Vcvv 3078    C_ wss 3433   {csn 3993   {cpr 3995   U.cuni 4213   class class class wbr 4417    |-> cmpt 4476    X. cxp 4844   `'ccnv 4845   dom cdm 4846   ran crn 4847   "cima 4849   Fun wfun 5587    Fn wfn 5588   -->wf 5589   ` cfv 5593  (class class class)co 6297    ^m cmap 7472   CCcc 9533   RRcr 9534   0cc0 9535   1c1 9536    + caddc 9538   RR*cxr 9670    < clt 9671    <_ cle 9672    - cmin 9856   -ucneg 9857   NNcn 10605   RR+crp 11298   (,)cioo 11631   [,]cicc 11634   ...cfz 11778   abscabs 13276   ↾t crest 15297   topGenctg 15314   Xt_cpt 15315    TosetRel ctsr 16423   Topctop 19894  TopOnctopon 19895    Cn ccn 20217    CnP ccnp 20218
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589  ax-inf2 8144  ax-cnex 9591  ax-resscn 9592  ax-1cn 9593  ax-icn 9594  ax-addcl 9595  ax-addrcl 9596  ax-mulcl 9597  ax-mulrcl 9598  ax-mulcom 9599  ax-addass 9600  ax-mulass 9601  ax-distr 9602  ax-i2m1 9603  ax-1ne0 9604  ax-1rid 9605  ax-rnegex 9606  ax-rrecex 9607  ax-cnre 9608  ax-pre-lttri 9609  ax-pre-lttrn 9610  ax-pre-ltadd 9611  ax-pre-mulgt0 9612  ax-pre-sup 9613
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-iin 4296  df-disj 4389  df-br 4418  df-opab 4477  df-mpt 4478  df-tr 4513  df-eprel 4757  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-se 4806  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-pred 5391  df-ord 5437  df-on 5438  df-lim 5439  df-suc 5440  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6259  df-ov 6300  df-oprab 6301  df-mpt2 6302  df-of 6537  df-om 6699  df-1st 6799  df-2nd 6800  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-omul 7187  df-er 7363  df-map 7474  df-pm 7475  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fi 7923  df-sup 7954  df-inf 7955  df-oi 8023  df-card 8370  df-acn 8373  df-cda 8594  df-pnf 9673  df-mnf 9674  df-xr 9675  df-ltxr 9676  df-le 9677  df-sub 9858  df-neg 9859  df-div 10266  df-nn 10606  df-2 10664  df-3 10665  df-n0 10866  df-z 10934  df-uz 11156  df-q 11261  df-rp 11299  df-xneg 11405  df-xadd 11406  df-xmul 11407  df-ioo 11635  df-icc 11638  df-fz 11779  df-fzo 11910  df-fl 12021  df-seq 12207  df-exp 12266  df-fac 12453  df-bc 12481  df-hash 12509  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-clim 13530  df-sum 13731  df-dvds 14284  df-rest 15299  df-topgen 15320  df-pt 15321  df-ps 16424  df-tsr 16425  df-psmet 18940  df-xmet 18941  df-met 18942  df-bl 18943  df-mopn 18944  df-top 19898  df-bases 19899  df-topon 19900  df-cld 20011  df-ntr 20012  df-cls 20013  df-lp 20129  df-cn 20220  df-cnp 20221  df-t1 20307  df-haus 20308  df-cmp 20379  df-tx 20554  df-hmeo 20747  df-hmph 20748  df-ii 21886
This theorem is referenced by:  broucube  31882
  Copyright terms: Public domain W3C validator