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 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ftalem3.5 ⊢ 𝐷 = { 𝑦 ∈ ℂ ∣ ( abs ‘ 𝑦 ) ≤ 𝑅 }
ftalem3.6 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
ftalem3.7 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
ftalem3.8 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
Assertion ftalem3 ( 𝜑 → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4 ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5 ftalem3.5 ⊢ 𝐷 = { 𝑦 ∈ ℂ ∣ ( abs ‘ 𝑦 ) ≤ 𝑅 }
6 ftalem3.6 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
7 ftalem3.7 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
8 ftalem3.8 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
9 5 ssrab3 ⊢ 𝐷 ⊆ ℂ
10 6 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
11 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐽 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
12 10 9 11 mp2an ⊢ ( 𝐽 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 )
13 12 toponunii ⊢ 𝐷 = ∪ ( 𝐽 ↾t 𝐷 )
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 ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
20 6 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
21 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
22 21 cnmetdval ⊢ ( ( 0 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 0 − 𝑦 ) ) )
23 17 22 mpan ⊢ ( 𝑦 ∈ ℂ → ( 0 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 0 − 𝑦 ) ) )
24 df-neg ⊢ - 𝑦 = ( 0 − 𝑦 )
25 24 fveq2i ⊢ ( abs ‘ - 𝑦 ) = ( abs ‘ ( 0 − 𝑦 ) )
26 absneg ⊢ ( 𝑦 ∈ ℂ → ( abs ‘ - 𝑦 ) = ( abs ‘ 𝑦 ) )
27 25 26 eqtr3id ⊢ ( 𝑦 ∈ ℂ → ( abs ‘ ( 0 − 𝑦 ) ) = ( abs ‘ 𝑦 ) )
28 23 27 eqtrd ⊢ ( 𝑦 ∈ ℂ → ( 0 ( abs ∘ − ) 𝑦 ) = ( abs ‘ 𝑦 ) )
29 28 breq1d ⊢ ( 𝑦 ∈ ℂ → ( ( 0 ( abs ∘ − ) 𝑦 ) ≤ 𝑅 ↔ ( abs ‘ 𝑦 ) ≤ 𝑅 ) )
30 29 rabbiia ⊢ { 𝑦 ∈ ℂ ∣ ( 0 ( abs ∘ − ) 𝑦 ) ≤ 𝑅 } = { 𝑦 ∈ ℂ ∣ ( abs ‘ 𝑦 ) ≤ 𝑅 }
31 5 30 eqtr4i ⊢ 𝐷 = { 𝑦 ∈ ℂ ∣ ( 0 ( abs ∘ − ) 𝑦 ) ≤ 𝑅 }
32 20 31 blcld ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
33 16 18 19 32 syl3anc ⊢ ( 𝜑 → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
34 7 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
35 fveq2 ⊢ ( 𝑦 = 𝑥 → ( abs ‘ 𝑦 ) = ( abs ‘ 𝑥 ) )
36 35 breq1d ⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ 𝑦 ) ≤ 𝑅 ↔ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
37 36 5 elrab2 ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
38 37 simprbi ⊢ ( 𝑥 ∈ 𝐷 → ( abs ‘ 𝑥 ) ≤ 𝑅 )
39 38 rgen ⊢ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑅
40 brralrspcev ⊢ ( ( 𝑅 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑅 ) → ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑠 )
41 34 39 40 sylancl ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑠 )
42 eqid ⊢ ( 𝐽 ↾t 𝐷 ) = ( 𝐽 ↾t 𝐷 )
43 6 42 cnheibor ⊢ ( 𝐷 ⊆ ℂ → ( ( 𝐽 ↾t 𝐷 ) ∈ Comp ↔ ( 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑠 ) ) )
44 9 43 ax-mp ⊢ ( ( 𝐽 ↾t 𝐷 ) ∈ Comp ↔ ( 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑠 ) )
45 33 41 44 sylanbrc ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐷 ) ∈ Comp )
46 plycn ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( ℂ –cn→ ℂ ) )
47 3 46 syl ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )
48 abscncf ⊢ abs ∈ ( ℂ –cn→ ℝ )
49 48 a1i ⊢ ( 𝜑 → abs ∈ ( ℂ –cn→ ℝ ) )
50 47 49 cncfco ⊢ ( 𝜑 → ( abs ∘ 𝐹 ) ∈ ( ℂ –cn→ ℝ ) )
51 ssid ⊢ ℂ ⊆ ℂ
52 ax-resscn ⊢ ℝ ⊆ ℂ
53 10 toponrestid ⊢ 𝐽 = ( 𝐽 ↾t ℂ )
54 6 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( 𝐽 ↾t ℝ )
55 6 53 54 cncfcn ⊢ ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) = ( 𝐽 Cn ( topGen ‘ ran (,) ) ) )
56 51 52 55 mp2an ⊢ ( ℂ –cn→ ℝ ) = ( 𝐽 Cn ( topGen ‘ ran (,) ) )
57 50 56 eleqtrdi ⊢ ( 𝜑 → ( abs ∘ 𝐹 ) ∈ ( 𝐽 Cn ( topGen ‘ ran (,) ) ) )
58 10 toponunii ⊢ ℂ = ∪ 𝐽
59 58 cnrest ⊢ ( ( ( abs ∘ 𝐹 ) ∈ ( 𝐽 Cn ( topGen ‘ ran (,) ) ) ∧ 𝐷 ⊆ ℂ ) → ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ∈ ( ( 𝐽 ↾t 𝐷 ) Cn ( topGen ‘ ran (,) ) ) )
60 57 9 59 sylancl ⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ∈ ( ( 𝐽 ↾t 𝐷 ) Cn ( topGen ‘ ran (,) ) ) )
61 7 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑅 )
62 fveq2 ⊢ ( 𝑦 = 0 → ( abs ‘ 𝑦 ) = ( abs ‘ 0 ) )
63 abs0 ⊢ ( abs ‘ 0 ) = 0
64 62 63 eqtrdi ⊢ ( 𝑦 = 0 → ( abs ‘ 𝑦 ) = 0 )
65 64 breq1d ⊢ ( 𝑦 = 0 → ( ( abs ‘ 𝑦 ) ≤ 𝑅 ↔ 0 ≤ 𝑅 ) )
66 65 5 elrab2 ⊢ ( 0 ∈ 𝐷 ↔ ( 0 ∈ ℂ ∧ 0 ≤ 𝑅 ) )
67 18 61 66 sylanbrc ⊢ ( 𝜑 → 0 ∈ 𝐷 )
68 67 ne0d ⊢ ( 𝜑 → 𝐷 ≠ ∅ )
69 13 14 45 60 68 evth2 ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) ≤ ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) )
70 fvres ⊢ ( 𝑧 ∈ 𝐷 → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) )
71 70 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) )
72 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
73 3 72 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝐹 : ℂ ⟶ ℂ )
75 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑧 ∈ 𝐷 )
76 9 75 sselid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑧 ∈ ℂ )
77 fvco3 ⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
78 74 76 77 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
79 71 78 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
80 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) )
81 80 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) )
82 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
83 9 82 sselid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℂ )
84 fvco3 ⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
85 74 83 84 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
86 81 85 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
87 79 86 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) ≤ ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
88 87 ralbidva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐷 ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) ≤ ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
89 88 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) ≤ ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
90 69 89 mpbid ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
91 ssrexv ⊢ ( 𝐷 ⊆ ℂ → ( ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
92 9 90 91 mpsyl ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
93 67 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 0 ∈ 𝐷 )
94 2fveq3 ⊢ ( 𝑥 = 0 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ 0 ) ) )
95 94 breq2d ⊢ ( 𝑥 = 0 → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ) )
96 95 rspcv ⊢ ( 0 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ) )
97 93 96 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ) )
98 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝐹 : ℂ ⟶ ℂ )
99 ffvelrn ⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 0 ∈ ℂ ) → ( 𝐹 ‘ 0 ) ∈ ℂ )
100 98 17 99 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝐹 ‘ 0 ) ∈ ℂ )
101 100 abscld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) ∈ ℝ )
102 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑥 ∈ ( ℂ ∖ 𝐷 ) )
103 102 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑥 ∈ ℂ )
104 98 103 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
105 104 abscld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
106 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ∀ 𝑥 ∈ ℂ ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
107 102 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ¬ 𝑥 ∈ 𝐷 )
108 37 baib ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ∈ 𝐷 ↔ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
109 103 108 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝑥 ∈ 𝐷 ↔ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
110 107 109 mtbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ¬ ( abs ‘ 𝑥 ) ≤ 𝑅 )
111 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑅 ∈ ℝ )
112 103 abscld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
113 111 112 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝑅 < ( abs ‘ 𝑥 ) ↔ ¬ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
114 110 113 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑅 < ( abs ‘ 𝑥 ) )
115 rsp ⊢ ( ∀ 𝑥 ∈ ℂ ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℂ → ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
116 106 103 114 115 syl3c ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
117 101 105 116 ltled ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
118 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑧 ∈ ℂ )
119 98 118 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
120 119 abscld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
121 letr ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 0 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 0 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
122 120 101 105 121 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 0 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
123 117 122 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
124 123 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) → ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
125 97 124 syld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
126 125 ancld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
127 ralunb ⊢ ( ∀ 𝑥 ∈ ( 𝐷 ∪ ( ℂ ∖ 𝐷 ) ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
128 undif2 ⊢ ( 𝐷 ∪ ( ℂ ∖ 𝐷 ) ) = ( 𝐷 ∪ ℂ )
129 ssequn1 ⊢ ( 𝐷 ⊆ ℂ ↔ ( 𝐷 ∪ ℂ ) = ℂ )
130 9 129 mpbi ⊢ ( 𝐷 ∪ ℂ ) = ℂ
131 128 130 eqtri ⊢ ( 𝐷 ∪ ( ℂ ∖ 𝐷 ) ) = ℂ
132 131 raleqi ⊢ ( ∀ 𝑥 ∈ ( 𝐷 ∪ ( ℂ ∖ 𝐷 ) ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
133 127 132 bitr3i ⊢ ( ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
134 126 133 syl6ib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
135 134 reximdva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
136 92 135 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )