# 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}=\mathrm{coeff}\left({F}\right)$
ftalem.2 ${⊢}{N}=\mathrm{deg}\left({F}\right)$
ftalem.3 ${⊢}{\phi }\to {F}\in \mathrm{Poly}\left({S}\right)$
ftalem.4 ${⊢}{\phi }\to {N}\in ℕ$
ftalem3.5 ${⊢}{D}=\left\{{y}\in ℂ|\left|{y}\right|\le {R}\right\}$
ftalem3.6 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
ftalem3.7 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
ftalem3.8 ${⊢}{\phi }\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left({R}<\left|{x}\right|\to \left|{F}\left(0\right)\right|<\left|{F}\left({x}\right)\right|\right)$
Assertion ftalem3 ${⊢}{\phi }\to \exists {z}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left|{F}\left({z}\right)\right|\le \left|{F}\left({x}\right)\right|$

### Proof

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