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 32037
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 32036 . 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 6336 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1 ... N )  e. 
_V
9 retopon 21862 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  (TopOn `  RR )
103pttoponconst 20689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 1 ... N
)  e.  _V  /\  ( topGen `  ran  (,) )  e.  (TopOn `  RR )
)  ->  R  e.  (TopOn `  ( RR  ^m  ( 1 ... N
) ) ) )
118, 9, 10mp2an 686 . . . . . . . . . . . . . . . . . . . . 21  |-  R  e.  (TopOn `  ( RR  ^m  ( 1 ... N
) ) )
1211topontopi 20023 . . . . . . . . . . . . . . . . . . . 20  |-  R  e. 
Top
13 reex 9648 . . . . . . . . . . . . . . . . . . . . . 22  |-  RR  e.  _V
14 unitssre 11805 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 [,] 1 )  C_  RR
15 mapss 7532 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  e.  _V  /\  ( 0 [,] 1
)  C_  RR )  ->  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) 
C_  ( RR  ^m  ( 1 ... N
) ) )
1613, 14, 15mp2an 686 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  C_  ( RR  ^m  (
1 ... N ) )
172, 16eqsstri 3448 . . . . . . . . . . . . . . . . . . . 20  |-  I  C_  ( RR  ^m  (
1 ... N ) )
1811toponunii 20024 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
^m  ( 1 ... N ) )  = 
U. R
1918restuni 20255 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  Top  /\  I  C_  ( RR  ^m  ( 1 ... N
) ) )  ->  I  =  U. ( Rt  I ) )
2012, 17, 19mp2an 686 . . . . . . . . . . . . . . . . . . 19  |-  I  = 
U. ( Rt  I )
2120, 18cnf 20339 . . . . . . . . . . . . . . . . . 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 6037 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  I )  ->  ( F `  c )  e.  ( RR  ^m  (
1 ... N ) ) )
24 elmapi 7511 . . . . . . . . . . . . . . . 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 6037 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( F `  c
) `  n )  e.  RR )
27 recn 9647 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( ( F `  c ) `  n )  e.  CC )
28 absrpcl 13428 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  CC  /\  ( ( F `  c ) `  n
)  =/=  0 )  ->  ( abs `  (
( F `  c
) `  n )
)  e.  RR+ )
2928ex 441 . . . . . . . . . . . . . . . . 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 11358 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR+ )  ->  (
( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) )  < 
( ( F `  c ) `  n
) )
32 ltaddrp 11359 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR+ )  ->  (
( F `  c
) `  n )  <  ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )
3331, 32jca 541 . . . . . . . . . . . . . . . . 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 441 . . . . . . . . . . . . . . . 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 44 . . . . . . . . . . . . . . 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 13575 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( abs `  ( ( F `  c ) `  n
) )  e.  RR )
37 resubcl 9958 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  e.  RR )
3836, 37mpdan 681 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  e.  RR )
3938rexrd 9708 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  e.  RR* )
40 readdcl 9640 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( abs `  ( ( F `  c ) `
 n ) )  e.  RR )  -> 
( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) )  e.  RR )
4136, 40mpdan 681 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  e.  RR )
4241rexrd 9708 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  e.  RR* )
43 rexr 9704 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( ( F `  c ) `  n )  e.  RR* )
44 elioo5 11717 . . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . 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 5879 . . . . . . . . . . . . . . . . 17  |-  ( x  =  c  ->  ( F `  x )  =  ( F `  c ) )
4948fveq1d 5881 . . . . . . . . . . . . . . . 16  |-  ( x  =  c  ->  (
( F `  x
) `  n )  =  ( ( F `
 c ) `  n ) )
50 eqid 2471 . . . . . . . . . . . . . . . 16  |-  ( x  e.  I  |->  ( ( F `  x ) `
 n ) )  =  ( x  e.  I  |->  ( ( F `
 x ) `  n ) )
51 fvex 5889 . . . . . . . . . . . . . . . 16  |-  ( ( F `  c ) `
 n )  e. 
_V
5249, 50, 51fvmpt 5963 . . . . . . . . . . . . . . 15  |-  ( c  e.  I  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  c
)  =  ( ( F `  c ) `
 n ) )
5352eleq1d 2533 . . . . . . . . . . . . . 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 741 . . . . . . . . . . . . 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 242 . . . . . . . . . . . 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 21864 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  c ) `  n
)  -  ( abs `  ( ( F `  c ) `  n
) ) ) (,) ( ( ( F `
 c ) `  n )  +  ( abs `  ( ( F `  c ) `
 n ) ) ) )  e.  (
topGen `  ran  (,) )
57 resttopon 20254 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  (TopOn `  ( RR  ^m  (
1 ... N ) ) )  /\  I  C_  ( RR  ^m  (
1 ... N ) ) )  ->  ( Rt  I
)  e.  (TopOn `  I ) )
5811, 17, 57mp2an 686 . . . . . . . . . . . . . . . . . . 19  |-  ( Rt  I )  e.  (TopOn `  I )
5958a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( Rt  I )  e.  (TopOn `  I ) )
6022feqmptd 5932 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  =  ( x  e.  I  |->  ( F `
 x ) ) )
6160, 4eqeltrrd 2550 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  I  |->  ( F `  x
) )  e.  ( ( Rt  I )  Cn  R
) )
6261adantr 472 . . . . . . . . . . . . . . . . . 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 21860 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
6564fconst6 5786 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Top
6618, 3ptpjcn 20703 . . . . . . . . . . . . . . . . . . . . 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 1380 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) ) )
68 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  _V
6968fvconst2 6136 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  =  ( topGen ` 
ran  (,) ) )
7069oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  ( R  Cn  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  =  ( R  Cn  ( topGen `  ran  (,) )
) )
7167, 70eleqtrd 2551 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( topGen `  ran  (,) ) ) )
7271adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
z  e.  ( RR 
^m  ( 1 ... N ) )  |->  ( z `  n ) )  e.  ( R  Cn  ( topGen `  ran  (,) ) ) )
73 fveq1 5878 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( F `  x )  ->  (
z `  n )  =  ( ( F `
 x ) `  n ) )
7459, 62, 63, 72, 73cnmpt11 20755 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( Rt  I )  Cn  ( topGen `
 ran  (,) )
) )
7520cncnpi 20371 . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  c  e.  I )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( ( Rt  I )  CnP  ( topGen `
 ran  (,) )
) `  c )
)
7776an32s 821 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  e.  ( ( ( Rt  I )  CnP  ( topGen `
 ran  (,) )
) `  c )
)
78 iscnp 20330 . . . . . . . . . . . . . . . . 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 1380 . . . . . . . . . . . . . . . 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 741 . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . 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 2538 . . . . . . . . . . . . . . 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 3440 . . . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . 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 2892 . . . . . . . . . . . . . . 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 327 . . . . . . . . . . . . . 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 3132 . . . . . . . . . . . . 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 64 . . . . . . . . . . . 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 44 . . . . . . . . . . 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 9661 . . . . . . . . . . . 12  |-  0  e.  RR
92 letric 9752 . . . . . . . . . . . 12  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  e.  RR )  ->  ( ( ( F `
 c ) `  n )  <_  0  \/  0  <_  ( ( F `  c ) `
 n ) ) )
9326, 91, 92sylancl 675 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( F `  c ) `  n
)  <_  0  \/  0  <_  ( ( F `
 c ) `  n ) ) )
9490, 93jctird 553 . . . . . . . . . 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 2928 . . . . . . . . . . 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 661 . . . . . . . . . . . 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 2881 . . . . . . . . . . 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 259 . . . . . . . . . 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 234 . . . . . . . . 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 20023 . . . . . . . . . . . . 13  |-  ( Rt  I )  e.  Top
10120eltopss 20014 . . . . . . . . . . . . 13  |-  ( ( ( Rt  I )  e.  Top  /\  v  e.  ( Rt  I ) )  ->  v  C_  I )
102100, 101mpan 684 . . . . . . . . . . . 12  |-  ( v  e.  ( Rt  I )  ->  v  C_  I
)
103 fvex 5889 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  x ) `
 n )  e. 
_V
104103, 50dmmpti 5717 . . . . . . . . . . . . . . . . 17  |-  dom  (
x  e.  I  |->  ( ( F `  x
) `  n )
)  =  I
105104sseq2i 3443 . . . . . . . . . . . . . . . 16  |-  ( v 
C_  dom  ( x  e.  I  |->  ( ( F `  x ) `
 n ) )  <-> 
v  C_  I )
106 funmpt 5625 . . . . . . . . . . . . . . . . 17  |-  Fun  (
x  e.  I  |->  ( ( F `  x
) `  n )
)
107 funimass4 5930 . . . . . . . . . . . . . . . . 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 684 . . . . . . . . . . . . . . . 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 218 . . . . . . . . . . . . . . 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 3413 . . . . . . . . . . . . . . . . 17  |-  ( ( v  C_  I  /\  z  e.  v )  ->  z  e.  I )
111 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
112111fveq1d 5881 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
( F `  x
) `  n )  =  ( ( F `
 z ) `  n ) )
113 fvex 5889 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  z ) `
 n )  e. 
_V
114112, 50, 113fvmpt 5963 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  I  ->  (
( x  e.  I  |->  ( ( F `  x ) `  n
) ) `  z
)  =  ( ( F `  z ) `
 n ) )
115114eleq1d 2533 . . . . . . . . . . . . . . . . . 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 11719 . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . 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 2805 . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . 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 13438 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( abs `  (
( F `  c
) `  n )
)  =  -u (
( F `  c
) `  n )
)
123122oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9995 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  +  -u ( ( F `
 c ) `  n ) )  =  0 )
125124adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( ( ( F `  c ) `
 n )  + 
-u ( ( F `
 c ) `  n ) )  =  0 )
126123, 125eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  ( ( F `  c ) `  n
)  <_  0 )  ->  ( ( ( F `  c ) `
 n )  +  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
12726, 126sylan 479 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  ( ( F `
 c ) `  n )  <_  0
)  ->  ( (
( F `  c
) `  n )  +  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
128127adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 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 4407 . . . . . . . . . . . . . . . . . . . . . . 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 6037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  I )  ->  ( F `  z )  e.  ( RR  ^m  (
1 ... N ) ) )
131 elmapi 7511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6037 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  I )  /\  n  e.  ( 1 ... N
) )  ->  (
( F `  z
) `  n )  e.  RR )
134133an32s 821 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
( F `  z
) `  n )  e.  RR )
135 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  0  e.  RR )
136134, 135ltnled 9799 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
( ( F `  z ) `  n
)  <  0  <->  -.  0  <_  ( ( F `  z ) `  n
) ) )
137136adantllr 733 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  z  e.  I
)  ->  ( (
( F `  z
) `  n )  <  0  <->  -.  0  <_  ( ( F `  z
) `  n )
) )
138137adantlr 729 . . . . . . . . . . . . . . . . . . . . . . 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 261 . . . . . . . . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . . . 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 2805 . . . . . . . . . . . . . . . . 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 821 . . . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . . 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 13436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( abs `  (
( F `  c
) `  n )
)  =  ( ( F `  c ) `
 n ) )
148147oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  =  ( ( ( F `  c ) `
 n )  -  ( ( F `  c ) `  n
) ) )
14927subidd 9993 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( F `  c
) `  n )  e.  RR  ->  ( (
( F `  c
) `  n )  -  ( ( F `
 c ) `  n ) )  =  0 )
150149adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  (
( F `  c
) `  n )
)  =  0 )
151148, 150eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( F `  c ) `  n
)  e.  RR  /\  0  <_  ( ( F `
 c ) `  n ) )  -> 
( ( ( F `
 c ) `  n )  -  ( abs `  ( ( F `
 c ) `  n ) ) )  =  0 )
15226, 151sylan 479 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  0  <_  (
( F `  c
) `  n )
)  ->  ( (
( F `  c
) `  n )  -  ( abs `  (
( F `  c
) `  n )
) )  =  0 )
153152adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 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 4405 . . . . . . . . . . . . . . . . . . . . . . 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 9799 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  z  e.  I )  ->  (
0  <  ( ( F `  z ) `  n )  <->  -.  (
( F `  z
) `  n )  <_  0 ) )
156155adantllr 733 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  c  e.  I )  /\  n  e.  (
1 ... N ) )  /\  z  e.  I
)  ->  ( 0  <  ( ( F `
 z ) `  n )  <->  -.  (
( F `  z
) `  n )  <_  0 ) )
157156adantlr 729 . . . . . . . . . . . . . . . . . . . . . . 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 261 . . . . . . . . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . . . . . . 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 2805 . . . . . . . . . . . . . . . . 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 821 . . . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . . 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 856 . . . . . . . . . . . . . 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 614 . . . . . . . . . . . . 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 489 . . . . . . . . . . . 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 482 . . . . . . . . . . 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 575 . . . . . . . . . 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 2858 . . . . . . . . 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 44 . . . . . . . 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 2834 . . . . . . . . . . . . . 14  |-  ( A. z  e.  v  -.  0 r ( ( F `  z ) `
 n )  <->  -.  E. z  e.  v  0 r ( ( F `  z ) `  n
) )
174173rexbii 2881 . . . . . . . . . . . . 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 16551 . . . . . . . . . . . . . . 15  |-  <_  e.  TosetRel
176175elexi 3041 . . . . . . . . . . . . . 14  |-  <_  e.  _V
177176cnvex 6759 . . . . . . . . . . . . . 14  |-  `'  <_  e. 
_V
178 breq 4397 . . . . . . . . . . . . . . . 16  |-  ( r  =  <_  ->  ( 0 r ( ( F `
 z ) `  n )  <->  0  <_  ( ( F `  z
) `  n )
) )
179178notbid 301 . . . . . . . . . . . . . . 15  |-  ( r  =  <_  ->  ( -.  0 r ( ( F `  z ) `
 n )  <->  -.  0  <_  ( ( F `  z ) `  n
) ) )
180179ralbidv 2829 . . . . . . . . . . . . . 14  |-  ( r  =  <_  ->  ( A. z  e.  v  -.  0 r ( ( F `  z ) `
 n )  <->  A. z  e.  v  -.  0  <_  ( ( F `  z ) `  n
) ) )
181 breq 4397 . . . . . . . . . . . . . . . . 17  |-  ( r  =  `'  <_  ->  ( 0 r ( ( F `  z ) `
 n )  <->  0 `'  <_  ( ( F `  z ) `  n
) ) )
182 c0ex 9655 . . . . . . . . . . . . . . . . . 18  |-  0  e.  _V
183182, 113brcnv 5022 . . . . . . . . . . . . . . . . 17  |-  ( 0 `'  <_  ( ( F `
 z ) `  n )  <->  ( ( F `  z ) `  n )  <_  0
)
184181, 183syl6bb 269 . . . . . . . . . . . . . . . 16  |-  ( r  =  `'  <_  ->  ( 0 r ( ( F `  z ) `
 n )  <->  ( ( F `  z ) `  n )  <_  0
) )
185184notbid 301 . . . . . . . . . . . . . . 15  |-  ( r  =  `'  <_  ->  ( -.  0 r ( ( F `  z
) `  n )  <->  -.  ( ( F `  z ) `  n
)  <_  0 ) )
186185ralbidv 2829 . . . . . . . . . . . . . 14  |-  ( r  =  `'  <_  ->  ( A. z  e.  v  -.  0 r ( ( F `  z
) `  n )  <->  A. z  e.  v  -.  ( ( F `  z ) `  n
)  <_  0 ) )
187176, 177, 180, 186rexpr 4017 . . . . . . . . . . . . 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 2836 . . . . . . . . . . . . 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 283 . . . . . . . . . . . 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 708 . . . . . . . . . . 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 432 . . . . . . . . . . 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 257 . . . . . . . . . 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 2881 . . . . . . . . 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 2836 . . . . . . . . 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 257 . . . . . . . 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 234 . . . . . . 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 2662 . . . . . 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 2805 . . . . 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 5739 . . . . . 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 552 . . . 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 6143 . . . . 5  |-  ( ( F `  c ) : ( 1 ... N ) --> { 0 }  <->  ( ( F `
 c )  Fn  ( 1 ... N
)  /\  A. n  e.  ( 1 ... N
) ( ( F `
 c ) `  n )  =  0 ) )
203182fconst2 6137 . . . . 5  |-  ( ( F `  c ) : ( 1 ... N ) --> { 0 }  <->  ( F `  c )  =  ( ( 1 ... N
)  X.  { 0 } ) )
204202, 203bitr3i 259 . . . 4  |-  ( ( ( F `  c
)  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( ( F `  c
) `  n )  =  0 )  <->  ( F `  c )  =  ( ( 1 ... N
)  X.  { 0 } ) )
205201, 204syl6ib 234 . . 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 2858 . 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 189    \/ wo 375    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031    C_ wss 3390   {csn 3959   {cpr 3961   U.cuni 4190   class class class wbr 4395    |-> cmpt 4454    X. cxp 4837   `'ccnv 4838   dom cdm 4839   ran crn 4840   "cima 4842   Fun wfun 5583    Fn wfn 5584   -->wf 5585   ` cfv 5589  (class class class)co 6308    ^m cmap 7490   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558    + caddc 9560   RR*cxr 9692    < clt 9693    <_ cle 9694    - cmin 9880   -ucneg 9881   NNcn 10631   RR+crp 11325   (,)cioo 11660   [,]cicc 11663   ...cfz 11810   abscabs 13374   ↾t crest 15397   topGenctg 15414   Xt_cpt 15415    TosetRel ctsr 16523   Topctop 19994  TopOnctopon 19995    Cn ccn 20317    CnP ccnp 20318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-omul 7205  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-acn 8394  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-sum 13830  df-dvds 14383  df-rest 15399  df-topgen 15420  df-pt 15421  df-ps 16524  df-tsr 16525  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-top 19998  df-bases 19999  df-topon 20000  df-cld 20111  df-ntr 20112  df-cls 20113  df-lp 20229  df-cn 20320  df-cnp 20321  df-t1 20407  df-haus 20408  df-cmp 20479  df-tx 20654  df-hmeo 20847  df-hmph 20848  df-ii 21987
This theorem is referenced by:  broucube  32038
  Copyright terms: Public domain W3C validator