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

Theorem poimir 31966
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 31965 . 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 6316 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1 ... N )  e. 
_V
9 retopon 21777 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  (TopOn `  RR )
103pttoponconst 20605 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 1 ... N
)  e.  _V  /\  ( topGen `  ran  (,) )  e.  (TopOn `  RR )
)  ->  R  e.  (TopOn `  ( RR  ^m  ( 1 ... N
) ) ) )
118, 9, 10mp2an 677 . . . . . . . . . . . . . . . . . . . . 21  |-  R  e.  (TopOn `  ( RR  ^m  ( 1 ... N
) ) )
1211topontopi 19939 . . . . . . . . . . . . . . . . . . . 20  |-  R  e. 
Top
13 reex 9627 . . . . . . . . . . . . . . . . . . . . . 22  |-  RR  e.  _V
14 unitssre 11776 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 [,] 1 )  C_  RR
15 mapss 7511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  e.  _V  /\  ( 0 [,] 1
)  C_  RR )  ->  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) 
C_  ( RR  ^m  ( 1 ... N
) ) )
1613, 14, 15mp2an 677 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  C_  ( RR  ^m  (
1 ... N ) )
172, 16eqsstri 3461 . . . . . . . . . . . . . . . . . . . 20  |-  I  C_  ( RR  ^m  (
1 ... N ) )
1811toponunii 19940 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
^m  ( 1 ... N ) )  = 
U. R
1918restuni 20171 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  Top  /\  I  C_  ( RR  ^m  ( 1 ... N
) ) )  ->  I  =  U. ( Rt  I ) )
2012, 17, 19mp2an 677 . . . . . . . . . . . . . . . . . . 19  |-  I  = 
U. ( Rt  I )
2120, 18cnf 20255 . . . . . . . . . . . . . . . . . 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 6020 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  I )  ->  ( F `  c )  e.  ( RR  ^m  (
1 ... N ) ) )
24 elmapi 7490 . . . . . . . . . . . . . . . 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 6020 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( F `  c
) `  n )  e.  RR )
27 recn 9626 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( ( F `  c ) `  n )  e.  CC )
28 absrpcl 13344 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  CC  /\  ( ( F `  c ) `  n
)  =/=  0 )  ->  ( abs `  (
( F `  c
) `  n )
)  e.  RR+ )
2928ex 436 . . . . . . . . . . . . . . . . 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 11332 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR+ )  ->  (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  < 
( ( F `  c ) `  n
) )
32 ltaddrp 11333 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR+ )  ->  (
( F `  c
) `  n )  <  ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )
3331, 32jca 535 . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . 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 13491 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( abs `  ( ( F `  c ) `  n
) )  e.  RR )
37 resubcl 9935 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  e.  RR )
3836, 37mpdan 673 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  e.  RR )
3938rexrd 9687 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  e.  RR* )
40 readdcl 9619 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR )  -> 
( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) )  e.  RR )
4136, 40mpdan 673 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  e.  RR )
4241rexrd 9687 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  e.  RR* )
43 rexr 9683 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( ( F `  c ) `  n )  e.  RR* )
44 elioo5 11689 . . . . . . . . . . . . . . . 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 1267 . . . . . . . . . . . . . . 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 238 . . . . . . . . . . . . . 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 5863 . . . . . . . . . . . . . . . . 17  |-  ( x  =  c  ->  ( F `  x )  =  ( F `  c ) )
4948fveq1d 5865 . . . . . . . . . . . . . . . 16  |-  ( x  =  c  ->  (
( F `  x
) `  n )  =  ( ( F `
 c ) `  n ) )
50 eqid 2450 . . . . . . . . . . . . . . . 16  |-  ( x  e.  I  |->  ( ( F `  x ) `
 n ) )  =  ( x  e.  I  |->  ( ( F `
 x ) `  n ) )
51 fvex 5873 . . . . . . . . . . . . . . . 16  |-  ( ( F `  c ) `
 n )  e. 
_V
5249, 50, 51fvmpt 5946 . . . . . . . . . . . . . . 15  |-  ( c  e.  I  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  c
)  =  ( ( F `  c ) `
 n ) )
5352eleq1d 2512 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . 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 238 . . . . . . . . . . . 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 21779 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )  e.  (
topGen `  ran  (,) )
57 resttopon 20170 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  (TopOn `  ( RR  ^m  (
1 ... N ) ) )  /\  I  C_  ( RR  ^m  (
1 ... N ) ) )  ->  ( Rt  I
)  e.  (TopOn `  I ) )
5811, 17, 57mp2an 677 . . . . . . . . . . . . . . . . . . 19  |-  ( Rt  I )  e.  (TopOn `  I )
5958a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( Rt  I )  e.  (TopOn `  I ) )
6022feqmptd 5916 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  =  ( x  e.  I  |->  ( F `
 x ) ) )
6160, 4eqeltrrd 2529 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  I  |->  ( F `  x
) )  e.  ( ( Rt  I )  Cn  R
) )
6261adantr 467 . . . . . . . . . . . . . . . . . 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 21775 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
6564fconst6 5771 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Top
6618, 3ptpjcn 20619 . . . . . . . . . . . . . . . . . . . . 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 1353 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) ) )
68 fvex 5873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  _V
6968fvconst2 6118 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  =  ( topGen ` 
ran  (,) ) )
7069oveq2d 6304 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  ( R  Cn  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  =  ( R  Cn  ( topGen `  ran  (,) )
) )
7167, 70eleqtrd 2530 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( topGen `  ran  (,) ) ) )
7271adantl 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( topGen `  ran  (,) ) ) )
73 fveq1 5862 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( F `  x )  ->  (
z `  n )  =  ( ( F `
 x ) `  n ) )
7459, 62, 63, 72, 73cnmpt11 20671 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( Rt  I )  Cn  ( topGen `
 ran  (,) )
) )
7520cncnpi 20287 . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  c  e.  I )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( ( Rt  I )  CnP  ( topGen `
 ran  (,) )
) `  c )
)
7776an32s 812 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( ( Rt  I )  CnP  ( topGen `
 ran  (,) )
) `  c )
)
78 iscnp 20246 . . . . . . . . . . . . . . . . 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 1353 . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . . 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 3453 . . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . 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 2900 . . . . . . . . . . . . . . 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 322 . . . . . . . . . . . . . 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 3145 . . . . . . . . . . . . 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 9640 . . . . . . . . . . . 12  |-  0  e.  RR
92 letric 9731 . . . . . . . . . . . 12  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  e.  RR )  ->  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) )
9326, 91, 92sylancl 667 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  <_  0  \/  0  <_  ( ( F `
 c ) `  n ) ) )
9490, 93jctird 547 . . . . . . . . . 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 2941 . . . . . . . . . . 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 654 . . . . . . . . . . . 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 2888 . . . . . . . . . . 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 255 . . . . . . . . . 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 230 . . . . . . . . 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 19939 . . . . . . . . . . . . 13  |-  ( Rt  I )  e.  Top
10120eltopss 19930 . . . . . . . . . . . . 13  |-  ( ( ( Rt  I )  e.  Top  /\  v  e.  ( Rt  I ) )  ->  v  C_  I )
102100, 101mpan 675 . . . . . . . . . . . 12  |-  ( v  e.  ( Rt  I )  ->  v  C_  I
)
103 fvex 5873 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  x ) `
 n )  e. 
_V
104103, 50dmmpti 5705 . . . . . . . . . . . . . . . . 17  |-  dom  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  =  I
105104sseq2i 3456 . . . . . . . . . . . . . . . 16  |-  ( v 
C_  dom  ( x  e.  I  |->  ( ( F `  x ) `
 n ) )  <-> 
v  C_  I )
106 funmpt 5617 . . . . . . . . . . . . . . . . 17  |-  Fun  (
x  e.  I  |->  ( ( F `  x
) `  n )
)
107 funimass4 5914 . . . . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . 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 3426 . . . . . . . . . . . . . . . . 17  |-  ( ( v  C_  I  /\  z  e.  v )  ->  z  e.  I )
111 fveq2 5863 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
112111fveq1d 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
( F `  x
) `  n )  =  ( ( F `
 z ) `  n ) )
113 fvex 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  z ) `
 n )  e. 
_V
114112, 50, 113fvmpt 5946 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  I  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  z
)  =  ( ( F `  z ) `
 n ) )
115114eleq1d 2512 . . . . . . . . . . . . . . . . . 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 11691 . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . . 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 2795 . . . . . . . . . . . . . . 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 219 . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . 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 13354 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( abs `  (
( F `  c
) `  n )
)  =  -u (
( F `  c
) `  n )
)
123122oveq2d 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9973 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  -u ( ( F `
 c ) `  n ) )  =  0 )
125124adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( ( ( F `  c ) `
 n )  + 
-u ( ( F `
 c ) `  n ) )  =  0 )
126123, 125eqtrd 2484 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
12726, 126sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  ( ( F `
 c ) `  n )  <_  0
)  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
128127adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 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 4413 . . . . . . . . . . . . . . . . . . . . . . 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 6020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  I )  ->  ( F `  z )  e.  ( RR  ^m  (
1 ... N ) ) )
131 elmapi 7490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( F `  z
) `  n )  e.  RR )
134133an32s 812 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
( F `  z
) `  n )  e.  RR )
135 0red 9641 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  0  e.  RR )
136134, 135ltnled 9779 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
( ( F `  z ) `  n
)  <  0  <->  -.  0  <_  ( ( F `  z ) `  n
) ) )
137136adantllr 724 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  z  e.  I
)  ->  ( (
( F `  z
) `  n )  <  0  <->  -.  0  <_  ( ( F `  z
) `  n )
) )
138137adantlr 720 . . . . . . . . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . . . . . . . . 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 211 . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . 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 653 . . . . . . . . . . . . . . . . . . 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 469 . . . . . . . . . . . . . . . . . 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 2795 . . . . . . . . . . . . . . . . 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 812 . . . . . . . . . . . . . . . 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 442 . . . . . . . . . . . . . . 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 13352 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( abs `  (
( F `  c
) `  n )
)  =  ( ( F `  c ) `
 n ) )
148147oveq2d 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  =  ( ( ( F `  c ) `
 n )  -  ( ( F `  c ) `  n
) ) )
14927subidd 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( ( F `
 c ) `  n ) )  =  0 )
150149adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  (
( F `  c
) `  n )
)  =  0 )
151148, 150eqtrd 2484 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  =  0 )
15226, 151sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  0  <_  (
( F `  c
) `  n )
)  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
153152adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 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 4411 . . . . . . . . . . . . . . . . . . . . . . 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 9779 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
0  <  ( ( F `  z ) `  n )  <->  -.  (
( F `  z
) `  n )  <_  0 ) )
156155adantllr 724 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  z  e.  I
)  ->  ( 0  <  ( ( F `
 z ) `  n )  <->  -.  (
( F `  z
) `  n )  <_  0 ) )
157156adantlr 720 . . . . . . . . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . . . . . . . . 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 211 . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . 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 653 . . . . . . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . . . . . . 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 2795 . . . . . . . . . . . . . . . . 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 812 . . . . . . . . . . . . . . . 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 442 . . . . . . . . . . . . . . 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 848 . . . . . . . . . . . . . 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 607 . . . . . . . . . . . . 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 484 . . . . . . . . . . . 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 477 . . . . . . . . . . 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 568 . . . . . . . . . 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 2861 . . . . . . . . 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 2833 . . . . . . . . . . . . . 14  |-  ( A. z  e.  v  -.  0 r ( ( F `  z ) `
 n )  <->  -.  E. z  e.  v  0 r ( ( F `  z ) `  n
) )
174173rexbii 2888 . . . . . . . . . . . . 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 16466 . . . . . . . . . . . . . . 15  |-  <_  e.  TosetRel
176175elexi 3054 . . . . . . . . . . . . . 14  |-  <_  e.  _V
177176cnvex 6737 . . . . . . . . . . . . . 14  |-  `'  <_  e. 
_V
178 breq 4403 . . . . . . . . . . . . . . . 16  |-  ( r  =  <_  ->  ( 0 r ( ( F `
 z ) `  n )  <->  0  <_  ( ( F `  z
) `  n )
) )
179178notbid 296 . . . . . . . . . . . . . . 15  |-  ( r  =  <_  ->  ( -.  0 r ( ( F `  z ) `
 n )  <->  -.  0  <_  ( ( F `  z ) `  n
) ) )
180179ralbidv 2826 . . . . . . . . . . . . . 14  |-  ( r  =  <_  ->  ( A. z  e.  v  -.  0 r ( ( F `  z ) `
 n )  <->  A. z  e.  v  -.  0  <_  ( ( F `  z ) `  n
) ) )
181 breq 4403 . . . . . . . . . . . . . . . . 17  |-  ( r  =  `'  <_  ->  ( 0 r ( ( F `  z ) `
 n )  <->  0 `'  <_  ( ( F `  z ) `  n
) ) )
182 c0ex 9634 . . . . . . . . . . . . . . . . . 18  |-  0  e.  _V
183182, 113brcnv 5016 . . . . . . . . . . . . . . . . 17  |-  ( 0 `'  <_  ( ( F `
 z ) `  n )  <->  ( ( F `  z ) `  n )  <_  0
)
184181, 183syl6bb 265 . . . . . . . . . . . . . . . 16  |-  ( r  =  `'  <_  ->  ( 0 r ( ( F `  z ) `
 n )  <->  ( ( F `  z ) `  n )  <_  0
) )
185184notbid 296 . . . . . . . . . . . . . . 15  |-  ( r  =  `'  <_  ->  ( -.  0 r ( ( F `  z
) `  n )  <->  -.  ( ( F `  z ) `  n
)  <_  0 ) )
186185ralbidv 2826 . . . . . . . . . . . . . 14  |-  ( r  =  `'  <_  ->  ( A. z  e.  v  -.  0 r ( ( F `  z
) `  n )  <->  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) )
187176, 177, 180, 186rexpr 4025 . . . . . . . . . . . . 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 2835 . . . . . . . . . . . . 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 279 . . . . . . . . . . . 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 699 . . . . . . . . . . 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 427 . . . . . . . . . . 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 253 . . . . . . . . . 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 2888 . . . . . . . . 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 2835 . . . . . . . . 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 253 . . . . . . . 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 230 . . . . . . 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 2795 . . . . 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 5726 . . . . . 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 546 . . . 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 6124 . . . . 5  |-  ( ( F `  c ) : ( 1 ... N ) --> { 0 }  <->  ( ( F `
 c )  Fn  ( 1 ... N
)  /\  A. n  e.  ( 1 ... N
) ( ( F `
 c ) `  n )  =  0 ) )
203182fconst2 6119 . . . . 5  |-  ( ( F `  c ) : ( 1 ... N ) --> { 0 }  <->  ( F `  c )  =  ( ( 1 ... N
)  X.  { 0 } ) )
204202, 203bitr3i 255 . . . 4  |-  ( ( ( F `  c
)  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( ( F `  c
) `  n )  =  0 )  <->  ( F `  c )  =  ( ( 1 ... N
)  X.  { 0 } ) )
205201, 204syl6ib 230 . . 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 2861 . 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 188    \/ wo 370    /\ wa 371    /\ w3a 984    = wceq 1443    e. wcel 1886    =/= wne 2621   A.wral 2736   E.wrex 2737   _Vcvv 3044    C_ wss 3403   {csn 3967   {cpr 3969   U.cuni 4197   class class class wbr 4401    |-> cmpt 4460    X. cxp 4831   `'ccnv 4832   dom cdm 4833   ran crn 4834   "cima 4836   Fun wfun 5575    Fn wfn 5576   -->wf 5577   ` cfv 5581  (class class class)co 6288    ^m cmap 7469   CCcc 9534   RRcr 9535   0cc0 9536   1c1 9537    + caddc 9539   RR*cxr 9671    < clt 9672    <_ cle 9673    - cmin 9857   -ucneg 9858   NNcn 10606   RR+crp 11299   (,)cioo 11632   [,]cicc 11635   ...cfz 11781   abscabs 13290   ↾t crest 15312   topGenctg 15329   Xt_cpt 15330    TosetRel ctsr 16438   Topctop 19910  TopOnctopon 19911    Cn ccn 20233    CnP ccnp 20234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-inf2 8143  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-fal 1449  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-iin 4280  df-disj 4373  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-of 6528  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-omul 7184  df-er 7360  df-map 7471  df-pm 7472  df-ixp 7520  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-fi 7922  df-sup 7953  df-inf 7954  df-oi 8022  df-card 8370  df-acn 8373  df-cda 8595  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-n0 10867  df-z 10935  df-uz 11157  df-q 11262  df-rp 11300  df-xneg 11406  df-xadd 11407  df-xmul 11408  df-ioo 11636  df-icc 11639  df-fz 11782  df-fzo 11913  df-fl 12025  df-seq 12211  df-exp 12270  df-fac 12457  df-bc 12485  df-hash 12513  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-clim 13545  df-sum 13746  df-dvds 14299  df-rest 15314  df-topgen 15335  df-pt 15336  df-ps 16439  df-tsr 16440  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-top 19914  df-bases 19915  df-topon 19916  df-cld 20027  df-ntr 20028  df-cls 20029  df-lp 20145  df-cn 20236  df-cnp 20237  df-t1 20323  df-haus 20324  df-cmp 20395  df-tx 20570  df-hmeo 20763  df-hmph 20764  df-ii 21902
This theorem is referenced by:  broucube  31967
  Copyright terms: Public domain W3C validator