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 φ F Poly S
ftalem.4 φ N
ftalem3.5 D = y | y R
ftalem3.6 J = TopOpen fld
ftalem3.7 φ R +
ftalem3.8 φ x R < x F 0 < F x
Assertion ftalem3 φ z x F z F x

Proof

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