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
|
syl5eqr |
⊢ ( 𝑦 ∈ ℂ → ( 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
|
sseldi |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑧 ∈ ℂ ) |
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
|
sseldi |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℂ ) |
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 ‘ ( 𝐹 ‘ 𝑥 ) ) ) |