Step |
Hyp |
Ref |
Expression |
1 |
|
poimir.0 |
|- ( ph -> N e. NN ) |
2 |
|
poimir.i |
|- I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) |
3 |
|
poimir.r |
|- R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) |
4 |
|
poimir.1 |
|- ( ph -> F e. ( ( R |`t I ) Cn R ) ) |
5 |
|
poimir.2 |
|- ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( F ` z ) ` n ) <_ 0 ) |
6 |
|
poimir.3 |
|- ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> 0 <_ ( ( F ` z ) ` n ) ) |
7 |
1 2 3 4 5 6
|
poimirlem32 |
|- ( ph -> E. c e. I A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) |
8 |
|
ovex |
|- ( 1 ... N ) e. _V |
9 |
|
retopon |
|- ( topGen ` ran (,) ) e. ( TopOn ` RR ) |
10 |
3
|
pttoponconst |
|- ( ( ( 1 ... N ) e. _V /\ ( topGen ` ran (,) ) e. ( TopOn ` RR ) ) -> R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) ) |
11 |
8 9 10
|
mp2an |
|- R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) |
12 |
11
|
topontopi |
|- R e. Top |
13 |
|
reex |
|- RR e. _V |
14 |
|
unitssre |
|- ( 0 [,] 1 ) C_ RR |
15 |
|
mapss |
|- ( ( RR e. _V /\ ( 0 [,] 1 ) C_ RR ) -> ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) ) ) |
16 |
13 14 15
|
mp2an |
|- ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) ) |
17 |
2 16
|
eqsstri |
|- I C_ ( RR ^m ( 1 ... N ) ) |
18 |
11
|
toponunii |
|- ( RR ^m ( 1 ... N ) ) = U. R |
19 |
18
|
restuni |
|- ( ( R e. Top /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> I = U. ( R |`t I ) ) |
20 |
12 17 19
|
mp2an |
|- I = U. ( R |`t I ) |
21 |
20 18
|
cnf |
|- ( F e. ( ( R |`t I ) Cn R ) -> F : I --> ( RR ^m ( 1 ... N ) ) ) |
22 |
4 21
|
syl |
|- ( ph -> F : I --> ( RR ^m ( 1 ... N ) ) ) |
23 |
22
|
ffvelrnda |
|- ( ( ph /\ c e. I ) -> ( F ` c ) e. ( RR ^m ( 1 ... N ) ) ) |
24 |
|
elmapi |
|- ( ( F ` c ) e. ( RR ^m ( 1 ... N ) ) -> ( F ` c ) : ( 1 ... N ) --> RR ) |
25 |
23 24
|
syl |
|- ( ( ph /\ c e. I ) -> ( F ` c ) : ( 1 ... N ) --> RR ) |
26 |
25
|
ffvelrnda |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` c ) ` n ) e. RR ) |
27 |
|
recn |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( F ` c ) ` n ) e. CC ) |
28 |
|
absrpcl |
|- ( ( ( ( F ` c ) ` n ) e. CC /\ ( ( F ` c ) ` n ) =/= 0 ) -> ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) |
29 |
28
|
ex |
|- ( ( ( F ` c ) ` n ) e. CC -> ( ( ( F ` c ) ` n ) =/= 0 -> ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) ) |
30 |
27 29
|
syl |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) =/= 0 -> ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) ) |
31 |
|
ltsubrp |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` c ) ` n ) ) |
32 |
|
ltaddrp |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) -> ( ( F ` c ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) |
33 |
31 32
|
jca |
|- ( ( ( ( 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 ) ) ) ) ) |
34 |
33
|
ex |
|- ( ( ( 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 ) ) ) ) ) ) |
35 |
30 34
|
syld |
|- ( ( ( 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 ) ) ) ) ) ) |
36 |
27
|
abscld |
|- ( ( ( F ` c ) ` n ) e. RR -> ( abs ` ( ( F ` c ) ` n ) ) e. RR ) |
37 |
|
resubcl |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) e. RR ) |
38 |
36 37
|
mpdan |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) e. RR ) |
39 |
38
|
rexrd |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) e. RR* ) |
40 |
|
readdcl |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) e. RR ) |
41 |
36 40
|
mpdan |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) e. RR ) |
42 |
41
|
rexrd |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) e. RR* ) |
43 |
|
rexr |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( F ` c ) ` n ) e. RR* ) |
44 |
|
elioo5 |
|- ( ( ( ( ( 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 ) ) ) ) ) ) |
45 |
39 42 43 44
|
syl3anc |
|- ( ( ( 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 ) ) ) ) ) ) |
46 |
35 45
|
sylibrd |
|- ( ( ( 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 ) ) ) ) ) ) |
47 |
26 46
|
syl |
|- ( ( ( 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 |
|- ( x = c -> ( F ` x ) = ( F ` c ) ) |
49 |
48
|
fveq1d |
|- ( x = c -> ( ( F ` x ) ` n ) = ( ( F ` c ) ` n ) ) |
50 |
|
eqid |
|- ( x e. I |-> ( ( F ` x ) ` n ) ) = ( x e. I |-> ( ( F ` x ) ` n ) ) |
51 |
|
fvex |
|- ( ( F ` c ) ` n ) e. _V |
52 |
49 50 51
|
fvmpt |
|- ( c e. I -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) = ( ( F ` c ) ` n ) ) |
53 |
52
|
eleq1d |
|- ( 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 ) ) ) ) ) ) |
54 |
53
|
ad2antlr |
|- ( ( ( 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 ) ) ) ) ) ) |
55 |
47 54
|
sylibrd |
|- ( ( ( 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 |
|- ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) e. ( topGen ` ran (,) ) |
57 |
|
resttopon |
|- ( ( R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> ( R |`t I ) e. ( TopOn ` I ) ) |
58 |
11 17 57
|
mp2an |
|- ( R |`t I ) e. ( TopOn ` I ) |
59 |
58
|
a1i |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( R |`t I ) e. ( TopOn ` I ) ) |
60 |
22
|
feqmptd |
|- ( ph -> F = ( x e. I |-> ( F ` x ) ) ) |
61 |
60 4
|
eqeltrrd |
|- ( ph -> ( x e. I |-> ( F ` x ) ) e. ( ( R |`t I ) Cn R ) ) |
62 |
61
|
adantr |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( F ` x ) ) e. ( ( R |`t I ) Cn R ) ) |
63 |
11
|
a1i |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) ) |
64 |
|
retop |
|- ( topGen ` ran (,) ) e. Top |
65 |
64
|
fconst6 |
|- ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top |
66 |
18 3
|
ptpjcn |
|- ( ( ( 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 ) ) ) |
67 |
8 65 66
|
mp3an12 |
|- ( n e. ( 1 ... N ) -> ( z e. ( RR ^m ( 1 ... N ) ) |-> ( z ` n ) ) e. ( R Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) ) |
68 |
|
fvex |
|- ( topGen ` ran (,) ) e. _V |
69 |
68
|
fvconst2 |
|- ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) = ( topGen ` ran (,) ) ) |
70 |
69
|
oveq2d |
|- ( n e. ( 1 ... N ) -> ( R Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) = ( R Cn ( topGen ` ran (,) ) ) ) |
71 |
67 70
|
eleqtrd |
|- ( n e. ( 1 ... N ) -> ( z e. ( RR ^m ( 1 ... N ) ) |-> ( z ` n ) ) e. ( R Cn ( topGen ` ran (,) ) ) ) |
72 |
71
|
adantl |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( z e. ( RR ^m ( 1 ... N ) ) |-> ( z ` n ) ) e. ( R Cn ( topGen ` ran (,) ) ) ) |
73 |
|
fveq1 |
|- ( z = ( F ` x ) -> ( z ` n ) = ( ( F ` x ) ` n ) ) |
74 |
59 62 63 72 73
|
cnmpt11 |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( R |`t I ) Cn ( topGen ` ran (,) ) ) ) |
75 |
20
|
cncnpi |
|- ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( R |`t I ) Cn ( topGen ` ran (,) ) ) /\ c e. I ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) ) |
76 |
74 75
|
sylan |
|- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ c e. I ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) ) |
77 |
76
|
an32s |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) ) |
78 |
|
iscnp |
|- ( ( ( R |`t I ) e. ( TopOn ` I ) /\ ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ c e. I ) -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t 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. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) ) ) |
79 |
58 9 78
|
mp3an12 |
|- ( c e. I -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t 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. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) ) ) |
80 |
79
|
ad2antlr |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t 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. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) ) ) |
81 |
77 80
|
mpbid |
|- ( ( ( 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. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) ) |
82 |
81
|
simprd |
|- ( ( ( 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. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) |
83 |
|
eleq2 |
|- ( 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 |
|- ( 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 ) ) ) ) ) ) |
85 |
84
|
anbi2d |
|- ( 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 ) ) ) ) ) ) ) |
86 |
85
|
rexbidv |
|- ( z = ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) <-> E. v e. ( R |`t 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 ) ) ) ) ) ) ) |
87 |
83 86
|
imbi12d |
|- ( 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. ( R |`t 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. ( R |`t 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 ) ) ) ) ) ) ) ) |
88 |
87
|
rspcv |
|- ( ( ( ( ( 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. ( R |`t 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. ( R |`t 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 ) ) ) ) ) ) ) ) |
89 |
56 82 88
|
mpsyl |
|- ( ( ( 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. ( R |`t 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 ) ) ) ) ) ) ) |
90 |
55 89
|
syld |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> E. v e. ( R |`t 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 |
|- 0 e. RR |
92 |
|
letric |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ 0 e. RR ) -> ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) |
93 |
26 91 92
|
sylancl |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) |
94 |
90 93
|
jctird |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> ( E. v e. ( R |`t 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 |
|- ( E. v e. ( R |`t 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. ( R |`t 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 |
|- ( ( ( 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 ) ) ) ) ) |
97 |
96
|
rexbii |
|- ( E. v e. ( R |`t 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. ( R |`t 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 ) ) ) ) ) |
98 |
95 97
|
bitr3i |
|- ( ( E. v e. ( R |`t 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. ( R |`t 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 ) ) ) ) ) |
99 |
94 98
|
syl6ib |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> E. v e. ( R |`t 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 ) ) ) ) ) ) |
100 |
58
|
topontopi |
|- ( R |`t I ) e. Top |
101 |
20
|
eltopss |
|- ( ( ( R |`t I ) e. Top /\ v e. ( R |`t I ) ) -> v C_ I ) |
102 |
100 101
|
mpan |
|- ( v e. ( R |`t I ) -> v C_ I ) |
103 |
|
fvex |
|- ( ( F ` x ) ` n ) e. _V |
104 |
103 50
|
dmmpti |
|- dom ( x e. I |-> ( ( F ` x ) ` n ) ) = I |
105 |
104
|
sseq2i |
|- ( v C_ dom ( x e. I |-> ( ( F ` x ) ` n ) ) <-> v C_ I ) |
106 |
|
funmpt |
|- Fun ( x e. I |-> ( ( F ` x ) ` n ) ) |
107 |
|
funimass4 |
|- ( ( 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 ) ) ) ) ) ) |
108 |
106 107
|
mpan |
|- ( 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 ) ) ) ) ) ) |
109 |
105 108
|
sylbir |
|- ( 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 |
|- ( ( v C_ I /\ z e. v ) -> z e. I ) |
111 |
|
fveq2 |
|- ( x = z -> ( F ` x ) = ( F ` z ) ) |
112 |
111
|
fveq1d |
|- ( x = z -> ( ( F ` x ) ` n ) = ( ( F ` z ) ` n ) ) |
113 |
|
fvex |
|- ( ( F ` z ) ` n ) e. _V |
114 |
112 50 113
|
fvmpt |
|- ( z e. I -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) = ( ( F ` z ) ` n ) ) |
115 |
114
|
eleq1d |
|- ( 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 |
|- ( ( ( 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 ) ) ) ) ) |
117 |
115 116
|
syl6bi |
|- ( 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 ) ) ) ) ) ) |
118 |
110 117
|
syl |
|- ( ( 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 ) ) ) ) ) ) |
119 |
118
|
ralimdva |
|- ( 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 ) ) ) ) ) ) |
120 |
109 119
|
sylbid |
|- ( 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 ) ) ) ) ) ) |
121 |
120
|
adantl |
|- ( ( ( ( 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 |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( abs ` ( ( F ` c ) ` n ) ) = -u ( ( F ` c ) ` n ) ) |
123 |
122
|
oveq2d |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) = ( ( ( F ` c ) ` n ) + -u ( ( F ` c ) ` n ) ) ) |
124 |
27
|
negidd |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) + -u ( ( F ` c ) ` n ) ) = 0 ) |
125 |
124
|
adantr |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( ( ( F ` c ) ` n ) + -u ( ( F ` c ) ` n ) ) = 0 ) |
126 |
123 125
|
eqtrd |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) = 0 ) |
127 |
26 126
|
sylan |
|- ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) = 0 ) |
128 |
127
|
adantr |
|- ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ z e. I ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) = 0 ) |
129 |
128
|
breq2d |
|- ( ( ( ( ( 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 ) ) |
130 |
22
|
ffvelrnda |
|- ( ( ph /\ z e. I ) -> ( F ` z ) e. ( RR ^m ( 1 ... N ) ) ) |
131 |
|
elmapi |
|- ( ( F ` z ) e. ( RR ^m ( 1 ... N ) ) -> ( F ` z ) : ( 1 ... N ) --> RR ) |
132 |
130 131
|
syl |
|- ( ( ph /\ z e. I ) -> ( F ` z ) : ( 1 ... N ) --> RR ) |
133 |
132
|
ffvelrnda |
|- ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` z ) ` n ) e. RR ) |
134 |
133
|
an32s |
|- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( ( F ` z ) ` n ) e. RR ) |
135 |
|
0red |
|- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> 0 e. RR ) |
136 |
134 135
|
ltnled |
|- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < 0 <-> -. 0 <_ ( ( F ` z ) ` n ) ) ) |
137 |
136
|
adantllr |
|- ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < 0 <-> -. 0 <_ ( ( F ` z ) ` n ) ) ) |
138 |
137
|
adantlr |
|- ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < 0 <-> -. 0 <_ ( ( F ` z ) ` n ) ) ) |
139 |
129 138
|
bitrd |
|- ( ( ( ( ( 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 ) ) ) |
140 |
139
|
biimpd |
|- ( ( ( ( ( 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 ) ) ) |
141 |
110 140
|
sylan2 |
|- ( ( ( ( ( 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 ) ) ) |
142 |
141
|
anassrs |
|- ( ( ( ( ( ( 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 ) ) ) |
143 |
142
|
adantld |
|- ( ( ( ( ( ( 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 ) ) ) |
144 |
143
|
ralimdva |
|- ( ( ( ( ( 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 ) ) ) |
145 |
144
|
an32s |
|- ( ( ( ( ( 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 ) ) ) |
146 |
145
|
impancom |
|- ( ( ( ( ( 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 |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( abs ` ( ( F ` c ) ` n ) ) = ( ( F ` c ) ` n ) ) |
148 |
147
|
oveq2d |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) = ( ( ( F ` c ) ` n ) - ( ( F ` c ) ` n ) ) ) |
149 |
27
|
subidd |
|- ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) - ( ( F ` c ) ` n ) ) = 0 ) |
150 |
149
|
adantr |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( ( ( F ` c ) ` n ) - ( ( F ` c ) ` n ) ) = 0 ) |
151 |
148 150
|
eqtrd |
|- ( ( ( ( F ` c ) ` n ) e. RR /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) = 0 ) |
152 |
26 151
|
sylan |
|- ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) = 0 ) |
153 |
152
|
adantr |
|- ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ z e. I ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) = 0 ) |
154 |
153
|
breq1d |
|- ( ( ( ( ( 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 ) ) ) |
155 |
135 134
|
ltnled |
|- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( 0 < ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) ) |
156 |
155
|
adantllr |
|- ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( 0 < ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) ) |
157 |
156
|
adantlr |
|- ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ z e. I ) -> ( 0 < ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) ) |
158 |
154 157
|
bitrd |
|- ( ( ( ( ( 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 ) ) |
159 |
158
|
biimpd |
|- ( ( ( ( ( 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 ) ) |
160 |
110 159
|
sylan2 |
|- ( ( ( ( ( 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 ) ) |
161 |
160
|
anassrs |
|- ( ( ( ( ( ( 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 ) ) |
162 |
161
|
adantrd |
|- ( ( ( ( ( ( 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 ) ) |
163 |
162
|
ralimdva |
|- ( ( ( ( ( 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 ) ) |
164 |
163
|
an32s |
|- ( ( ( ( ( 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 ) ) |
165 |
164
|
impancom |
|- ( ( ( ( ( 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 ) ) |
166 |
146 165
|
orim12d |
|- ( ( ( ( ( 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 ) ) ) |
167 |
166
|
expimpd |
|- ( ( ( ( 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 ) ) ) |
168 |
121 167
|
syland |
|- ( ( ( ( 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 ) ) ) |
169 |
102 168
|
sylan2 |
|- ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v e. ( R |`t 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 ) ) ) |
170 |
169
|
anim2d |
|- ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v e. ( R |`t 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 ) ) ) ) |
171 |
170
|
reximdva |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( E. v e. ( R |`t 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. ( R |`t I ) ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) ) ) |
172 |
99 171
|
syld |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> E. v e. ( R |`t I ) ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) ) ) |
173 |
|
ralnex |
|- ( A. z e. v -. 0 r ( ( F ` z ) ` n ) <-> -. E. z e. v 0 r ( ( F ` z ) ` n ) ) |
174 |
173
|
rexbii |
|- ( 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 |
|- <_ e. TosetRel |
176 |
175
|
elexi |
|- <_ e. _V |
177 |
176
|
cnvex |
|- `' <_ e. _V |
178 |
|
breq |
|- ( r = <_ -> ( 0 r ( ( F ` z ) ` n ) <-> 0 <_ ( ( F ` z ) ` n ) ) ) |
179 |
178
|
notbid |
|- ( r = <_ -> ( -. 0 r ( ( F ` z ) ` n ) <-> -. 0 <_ ( ( F ` z ) ` n ) ) ) |
180 |
179
|
ralbidv |
|- ( r = <_ -> ( A. z e. v -. 0 r ( ( F ` z ) ` n ) <-> A. z e. v -. 0 <_ ( ( F ` z ) ` n ) ) ) |
181 |
|
breq |
|- ( r = `' <_ -> ( 0 r ( ( F ` z ) ` n ) <-> 0 `' <_ ( ( F ` z ) ` n ) ) ) |
182 |
|
c0ex |
|- 0 e. _V |
183 |
182 113
|
brcnv |
|- ( 0 `' <_ ( ( F ` z ) ` n ) <-> ( ( F ` z ) ` n ) <_ 0 ) |
184 |
181 183
|
syl6bb |
|- ( r = `' <_ -> ( 0 r ( ( F ` z ) ` n ) <-> ( ( F ` z ) ` n ) <_ 0 ) ) |
185 |
184
|
notbid |
|- ( r = `' <_ -> ( -. 0 r ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) ) |
186 |
185
|
ralbidv |
|- ( r = `' <_ -> ( A. z e. v -. 0 r ( ( F ` z ) ` n ) <-> A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) |
187 |
176 177 180 186
|
rexpr |
|- ( 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 |
|- ( E. r e. { <_ , `' <_ } -. E. z e. v 0 r ( ( F ` z ) ` n ) <-> -. A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) |
189 |
174 187 188
|
3bitr3i |
|- ( ( 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 ) ) |
190 |
189
|
anbi2i |
|- ( ( 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 |
|- ( ( 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 ) ) ) |
192 |
190 191
|
bitri |
|- ( ( 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 ) ) ) |
193 |
192
|
rexbii |
|- ( E. v e. ( R |`t I ) ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) <-> E. v e. ( R |`t I ) -. ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) |
194 |
|
rexnal |
|- ( E. v e. ( R |`t I ) -. ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) <-> -. A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) |
195 |
193 194
|
bitri |
|- ( E. v e. ( R |`t I ) ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) <-> -. A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) |
196 |
172 195
|
syl6ib |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> -. A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) ) |
197 |
196
|
necon4ad |
|- ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) -> ( ( F ` c ) ` n ) = 0 ) ) |
198 |
197
|
ralimdva |
|- ( ( ph /\ c e. I ) -> ( A. n e. ( 1 ... N ) A. v e. ( R |`t 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 |
25
|
ffnd |
|- ( ( ph /\ c e. I ) -> ( F ` c ) Fn ( 1 ... N ) ) |
200 |
198 199
|
jctild |
|- ( ( ph /\ c e. I ) -> ( A. n e. ( 1 ... N ) A. v e. ( R |`t 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 ) ) ) |
201 |
|
fconstfv |
|- ( ( F ` c ) : ( 1 ... N ) --> { 0 } <-> ( ( F ` c ) Fn ( 1 ... N ) /\ A. n e. ( 1 ... N ) ( ( F ` c ) ` n ) = 0 ) ) |
202 |
182
|
fconst2 |
|- ( ( F ` c ) : ( 1 ... N ) --> { 0 } <-> ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) ) |
203 |
201 202
|
bitr3i |
|- ( ( ( F ` c ) Fn ( 1 ... N ) /\ A. n e. ( 1 ... N ) ( ( F ` c ) ` n ) = 0 ) <-> ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) ) |
204 |
200 203
|
syl6ib |
|- ( ( ph /\ c e. I ) -> ( A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) -> ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) ) ) |
205 |
204
|
reximdva |
|- ( ph -> ( E. c e. I A. n e. ( 1 ... N ) A. v e. ( R |`t 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 } ) ) ) |
206 |
7 205
|
mpd |
|- ( ph -> E. c e. I ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) ) |