Metamath Proof Explorer

Theorem ftalem3

Description: Lemma for fta . There exists a global minimum of the function abs o. F . The proof uses a circle of radius r where r is the value coming from ftalem1 ; since this is a compact set, the minimum on this disk is achieved, and this must then be the global minimum. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses ftalem.1 
|- A = ( coeff ` F )
ftalem.2 
|- N = ( deg ` F )
ftalem.3 
|- ( ph -> F e. ( Poly ` S ) )
ftalem.4 
|- ( ph -> N e. NN )
ftalem3.5 
|- D = { y e. CC | ( abs ` y ) <_ R }
ftalem3.6 
|- J = ( TopOpen ` CCfld )
ftalem3.7 
|- ( ph -> R e. RR+ )
ftalem3.8 
|- ( ph -> A. x e. CC ( R < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
Assertion ftalem3 
|- ( ph -> E. z e. CC A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 
 |-  A = ( coeff ` F )
2 ftalem.2 
 |-  N = ( deg ` F )
3 ftalem.3 
 |-  ( ph -> F e. ( Poly ` S ) )
4 ftalem.4 
 |-  ( ph -> N e. NN )
5 ftalem3.5 
 |-  D = { y e. CC | ( abs ` y ) <_ R }
6 ftalem3.6 
 |-  J = ( TopOpen ` CCfld )
7 ftalem3.7 
 |-  ( ph -> R e. RR+ )
8 ftalem3.8 
 |-  ( ph -> A. x e. CC ( R < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
9 5 ssrab3 
 |-  D C_ CC
10 6 cnfldtopon 
 |-  J e. ( TopOn ` CC )
11 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ D C_ CC ) -> ( J |`t D ) e. ( TopOn ` D ) )
12 10 9 11 mp2an 
 |-  ( J |`t D ) e. ( TopOn ` D )
13 12 toponunii 
 |-  D = U. ( J |`t D )
14 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
15 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
16 15 a1i 
 |-  ( ph -> ( abs o. - ) e. ( *Met ` CC ) )
17 0cn 
 |-  0 e. CC
18 17 a1i 
 |-  ( ph -> 0 e. CC )
19 7 rpxrd 
 |-  ( ph -> R e. RR* )
20 6 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
21 eqid 
 |-  ( abs o. - ) = ( abs o. - )
22 21 cnmetdval 
 |-  ( ( 0 e. CC /\ y e. CC ) -> ( 0 ( abs o. - ) y ) = ( abs ` ( 0 - y ) ) )
23 17 22 mpan 
 |-  ( y e. CC -> ( 0 ( abs o. - ) y ) = ( abs ` ( 0 - y ) ) )
24 df-neg 
 |-  -u y = ( 0 - y )
25 24 fveq2i 
 |-  ( abs ` -u y ) = ( abs ` ( 0 - y ) )
26 absneg 
 |-  ( y e. CC -> ( abs ` -u y ) = ( abs ` y ) )
27 25 26 eqtr3id 
 |-  ( y e. CC -> ( abs ` ( 0 - y ) ) = ( abs ` y ) )
28 23 27 eqtrd 
 |-  ( y e. CC -> ( 0 ( abs o. - ) y ) = ( abs ` y ) )
29 28 breq1d 
 |-  ( y e. CC -> ( ( 0 ( abs o. - ) y ) <_ R <-> ( abs ` y ) <_ R ) )
30 29 rabbiia 
 |-  { y e. CC | ( 0 ( abs o. - ) y ) <_ R } = { y e. CC | ( abs ` y ) <_ R }
31 5 30 eqtr4i 
 |-  D = { y e. CC | ( 0 ( abs o. - ) y ) <_ R }
32 20 31 blcld 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ R e. RR* ) -> D e. ( Clsd ` J ) )
33 16 18 19 32 syl3anc 
 |-  ( ph -> D e. ( Clsd ` J ) )
34 7 rpred 
 |-  ( ph -> R e. RR )
35 fveq2 
 |-  ( y = x -> ( abs ` y ) = ( abs ` x ) )
36 35 breq1d 
 |-  ( y = x -> ( ( abs ` y ) <_ R <-> ( abs ` x ) <_ R ) )
37 36 5 elrab2 
 |-  ( x e. D <-> ( x e. CC /\ ( abs ` x ) <_ R ) )
38 37 simprbi 
 |-  ( x e. D -> ( abs ` x ) <_ R )
39 38 rgen 
 |-  A. x e. D ( abs ` x ) <_ R
40 brralrspcev 
 |-  ( ( R e. RR /\ A. x e. D ( abs ` x ) <_ R ) -> E. s e. RR A. x e. D ( abs ` x ) <_ s )
41 34 39 40 sylancl 
 |-  ( ph -> E. s e. RR A. x e. D ( abs ` x ) <_ s )
42 eqid 
 |-  ( J |`t D ) = ( J |`t D )
43 6 42 cnheibor 
 |-  ( D C_ CC -> ( ( J |`t D ) e. Comp <-> ( D e. ( Clsd ` J ) /\ E. s e. RR A. x e. D ( abs ` x ) <_ s ) ) )
44 9 43 ax-mp 
 |-  ( ( J |`t D ) e. Comp <-> ( D e. ( Clsd ` J ) /\ E. s e. RR A. x e. D ( abs ` x ) <_ s ) )
45 33 41 44 sylanbrc 
 |-  ( ph -> ( J |`t D ) e. Comp )
46 plycn 
 |-  ( F e. ( Poly ` S ) -> F e. ( CC -cn-> CC ) )
47 3 46 syl 
 |-  ( ph -> F e. ( CC -cn-> CC ) )
48 abscncf 
 |-  abs e. ( CC -cn-> RR )
49 48 a1i 
 |-  ( ph -> abs e. ( CC -cn-> RR ) )
50 47 49 cncfco 
 |-  ( ph -> ( abs o. F ) e. ( CC -cn-> RR ) )
51 ssid 
 |-  CC C_ CC
52 ax-resscn 
 |-  RR C_ CC
53 10 toponrestid 
 |-  J = ( J |`t CC )
54 6 tgioo2 
 |-  ( topGen ` ran (,) ) = ( J |`t RR )
55 6 53 54 cncfcn 
 |-  ( ( CC C_ CC /\ RR C_ CC ) -> ( CC -cn-> RR ) = ( J Cn ( topGen ` ran (,) ) ) )
56 51 52 55 mp2an 
 |-  ( CC -cn-> RR ) = ( J Cn ( topGen ` ran (,) ) )
57 50 56 eleqtrdi 
 |-  ( ph -> ( abs o. F ) e. ( J Cn ( topGen ` ran (,) ) ) )
58 10 toponunii 
 |-  CC = U. J
59 58 cnrest 
 |-  ( ( ( abs o. F ) e. ( J Cn ( topGen ` ran (,) ) ) /\ D C_ CC ) -> ( ( abs o. F ) |` D ) e. ( ( J |`t D ) Cn ( topGen ` ran (,) ) ) )
60 57 9 59 sylancl 
 |-  ( ph -> ( ( abs o. F ) |` D ) e. ( ( J |`t D ) Cn ( topGen ` ran (,) ) ) )
61 7 rpge0d 
 |-  ( ph -> 0 <_ R )
62 fveq2 
 |-  ( y = 0 -> ( abs ` y ) = ( abs ` 0 ) )
63 abs0 
 |-  ( abs ` 0 ) = 0
64 62 63 eqtrdi 
 |-  ( y = 0 -> ( abs ` y ) = 0 )
65 64 breq1d 
 |-  ( y = 0 -> ( ( abs ` y ) <_ R <-> 0 <_ R ) )
66 65 5 elrab2 
 |-  ( 0 e. D <-> ( 0 e. CC /\ 0 <_ R ) )
67 18 61 66 sylanbrc 
 |-  ( ph -> 0 e. D )
68 67 ne0d 
 |-  ( ph -> D =/= (/) )
69 13 14 45 60 68 evth2 
 |-  ( ph -> E. z e. D A. x e. D ( ( ( abs o. F ) |` D ) ` z ) <_ ( ( ( abs o. F ) |` D ) ` x ) )
70 fvres 
 |-  ( z e. D -> ( ( ( abs o. F ) |` D ) ` z ) = ( ( abs o. F ) ` z ) )
71 70 ad2antlr 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> ( ( ( abs o. F ) |` D ) ` z ) = ( ( abs o. F ) ` z ) )
72 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
73 3 72 syl 
 |-  ( ph -> F : CC --> CC )
74 73 ad2antrr 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> F : CC --> CC )
75 simplr 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> z e. D )
76 9 75 sseldi 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> z e. CC )
77 fvco3 
 |-  ( ( F : CC --> CC /\ z e. CC ) -> ( ( abs o. F ) ` z ) = ( abs ` ( F ` z ) ) )
78 74 76 77 syl2anc 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> ( ( abs o. F ) ` z ) = ( abs ` ( F ` z ) ) )
79 71 78 eqtrd 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> ( ( ( abs o. F ) |` D ) ` z ) = ( abs ` ( F ` z ) ) )
80 fvres 
 |-  ( x e. D -> ( ( ( abs o. F ) |` D ) ` x ) = ( ( abs o. F ) ` x ) )
81 80 adantl 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> ( ( ( abs o. F ) |` D ) ` x ) = ( ( abs o. F ) ` x ) )
82 simpr 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> x e. D )
83 9 82 sseldi 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> x e. CC )
84 fvco3 
 |-  ( ( F : CC --> CC /\ x e. CC ) -> ( ( abs o. F ) ` x ) = ( abs ` ( F ` x ) ) )
85 74 83 84 syl2anc 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> ( ( abs o. F ) ` x ) = ( abs ` ( F ` x ) ) )
86 81 85 eqtrd 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> ( ( ( abs o. F ) |` D ) ` x ) = ( abs ` ( F ` x ) ) )
87 79 86 breq12d 
 |-  ( ( ( ph /\ z e. D ) /\ x e. D ) -> ( ( ( ( abs o. F ) |` D ) ` z ) <_ ( ( ( abs o. F ) |` D ) ` x ) <-> ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
88 87 ralbidva 
 |-  ( ( ph /\ z e. D ) -> ( A. x e. D ( ( ( abs o. F ) |` D ) ` z ) <_ ( ( ( abs o. F ) |` D ) ` x ) <-> A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
89 88 rexbidva 
 |-  ( ph -> ( E. z e. D A. x e. D ( ( ( abs o. F ) |` D ) ` z ) <_ ( ( ( abs o. F ) |` D ) ` x ) <-> E. z e. D A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
90 69 89 mpbid 
 |-  ( ph -> E. z e. D A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )
91 ssrexv 
 |-  ( D C_ CC -> ( E. z e. D A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> E. z e. CC A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
92 9 90 91 mpsyl 
 |-  ( ph -> E. z e. CC A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )
93 67 adantr 
 |-  ( ( ph /\ z e. CC ) -> 0 e. D )
94 2fveq3 
 |-  ( x = 0 -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` 0 ) ) )
95 94 breq2d 
 |-  ( x = 0 -> ( ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) <-> ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` 0 ) ) ) )
96 95 rspcv 
 |-  ( 0 e. D -> ( A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` 0 ) ) ) )
97 93 96 syl 
 |-  ( ( ph /\ z e. CC ) -> ( A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` 0 ) ) ) )
98 73 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> F : CC --> CC )
99 ffvelrn 
 |-  ( ( F : CC --> CC /\ 0 e. CC ) -> ( F ` 0 ) e. CC )
100 98 17 99 sylancl 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( F ` 0 ) e. CC )
101 100 abscld 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( abs ` ( F ` 0 ) ) e. RR )
102 simpr 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> x e. ( CC \ D ) )
103 102 eldifad 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> x e. CC )
104 98 103 ffvelrnd 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( F ` x ) e. CC )
105 104 abscld 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( abs ` ( F ` x ) ) e. RR )
106 8 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> A. x e. CC ( R < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
107 102 eldifbd 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> -. x e. D )
108 37 baib 
 |-  ( x e. CC -> ( x e. D <-> ( abs ` x ) <_ R ) )
109 103 108 syl 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( x e. D <-> ( abs ` x ) <_ R ) )
110 107 109 mtbid 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> -. ( abs ` x ) <_ R )
111 34 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> R e. RR )
112 103 abscld 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( abs ` x ) e. RR )
113 111 112 ltnled 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( R < ( abs ` x ) <-> -. ( abs ` x ) <_ R ) )
114 110 113 mpbird 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> R < ( abs ` x ) )
115 rsp 
 |-  ( A. x e. CC ( R < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) -> ( x e. CC -> ( R < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) )
116 106 103 114 115 syl3c 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) )
117 101 105 116 ltled 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( abs ` ( F ` 0 ) ) <_ ( abs ` ( F ` x ) ) )
118 simplr 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> z e. CC )
119 98 118 ffvelrnd 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( F ` z ) e. CC )
120 119 abscld 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( abs ` ( F ` z ) ) e. RR )
121 letr 
 |-  ( ( ( abs ` ( F ` z ) ) e. RR /\ ( abs ` ( F ` 0 ) ) e. RR /\ ( abs ` ( F ` x ) ) e. RR ) -> ( ( ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` 0 ) ) /\ ( abs ` ( F ` 0 ) ) <_ ( abs ` ( F ` x ) ) ) -> ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
122 120 101 105 121 syl3anc 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( ( ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` 0 ) ) /\ ( abs ` ( F ` 0 ) ) <_ ( abs ` ( F ` x ) ) ) -> ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
123 117 122 mpan2d 
 |-  ( ( ( ph /\ z e. CC ) /\ x e. ( CC \ D ) ) -> ( ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` 0 ) ) -> ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
124 123 ralrimdva 
 |-  ( ( ph /\ z e. CC ) -> ( ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` 0 ) ) -> A. x e. ( CC \ D ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
125 97 124 syld 
 |-  ( ( ph /\ z e. CC ) -> ( A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> A. x e. ( CC \ D ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
126 125 ancld 
 |-  ( ( ph /\ z e. CC ) -> ( A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> ( A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) /\ A. x e. ( CC \ D ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) ) )
127 ralunb 
 |-  ( A. x e. ( D u. ( CC \ D ) ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) <-> ( A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) /\ A. x e. ( CC \ D ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
128 undif2 
 |-  ( D u. ( CC \ D ) ) = ( D u. CC )
129 ssequn1 
 |-  ( D C_ CC <-> ( D u. CC ) = CC )
130 9 129 mpbi 
 |-  ( D u. CC ) = CC
131 128 130 eqtri 
 |-  ( D u. ( CC \ D ) ) = CC
132 131 raleqi 
 |-  ( A. x e. ( D u. ( CC \ D ) ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) <-> A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )
133 127 132 bitr3i 
 |-  ( ( A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) /\ A. x e. ( CC \ D ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) <-> A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )
134 126 133 syl6ib 
 |-  ( ( ph /\ z e. CC ) -> ( A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
135 134 reximdva 
 |-  ( ph -> ( E. z e. CC A. x e. D ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) -> E. z e. CC A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) ) )
136 92 135 mpd 
 |-  ( ph -> E. z e. CC A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )