Step | Hyp | Ref
| Expression |
1 | | ftalem3.5 |
. . . 4
⊢ 𝐷 = {𝑦 ∈ ℂ ∣ (abs‘𝑦) ≤ 𝑅} |
2 | 1 | ssrab3 4015 |
. . 3
⊢ 𝐷 ⊆
ℂ |
3 | | ftalem3.6 |
. . . . . . . 8
⊢ 𝐽 =
(TopOpen‘ℂfld) |
4 | 3 | cnfldtopon 23946 |
. . . . . . 7
⊢ 𝐽 ∈
(TopOn‘ℂ) |
5 | | resttopon 22312 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐷 ⊆ ℂ)
→ (𝐽
↾t 𝐷)
∈ (TopOn‘𝐷)) |
6 | 4, 2, 5 | mp2an 689 |
. . . . . 6
⊢ (𝐽 ↾t 𝐷) ∈ (TopOn‘𝐷) |
7 | 6 | toponunii 22065 |
. . . . 5
⊢ 𝐷 = ∪
(𝐽 ↾t
𝐷) |
8 | | eqid 2738 |
. . . . 5
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
9 | | cnxmet 23936 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
11 | | 0cn 10967 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℂ) |
13 | | ftalem3.7 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
14 | 13 | rpxrd 12773 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
15 | 3 | cnfldtopn 23945 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
16 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) |
17 | 16 | cnmetdval 23934 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℂ ∧ 𝑦
∈ ℂ) → (0(abs ∘ − )𝑦) = (abs‘(0 − 𝑦))) |
18 | 11, 17 | mpan 687 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → (0(abs
∘ − )𝑦) =
(abs‘(0 − 𝑦))) |
19 | | df-neg 11208 |
. . . . . . . . . . . . . 14
⊢ -𝑦 = (0 − 𝑦) |
20 | 19 | fveq2i 6777 |
. . . . . . . . . . . . 13
⊢
(abs‘-𝑦) =
(abs‘(0 − 𝑦)) |
21 | | absneg 14989 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ →
(abs‘-𝑦) =
(abs‘𝑦)) |
22 | 20, 21 | eqtr3id 2792 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ →
(abs‘(0 − 𝑦)) =
(abs‘𝑦)) |
23 | 18, 22 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → (0(abs
∘ − )𝑦) =
(abs‘𝑦)) |
24 | 23 | breq1d 5084 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → ((0(abs
∘ − )𝑦) ≤
𝑅 ↔ (abs‘𝑦) ≤ 𝑅)) |
25 | 24 | rabbiia 3407 |
. . . . . . . . 9
⊢ {𝑦 ∈ ℂ ∣ (0(abs
∘ − )𝑦) ≤
𝑅} = {𝑦 ∈ ℂ ∣ (abs‘𝑦) ≤ 𝑅} |
26 | 1, 25 | eqtr4i 2769 |
. . . . . . . 8
⊢ 𝐷 = {𝑦 ∈ ℂ ∣ (0(abs ∘
− )𝑦) ≤ 𝑅} |
27 | 15, 26 | blcld 23661 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑅 ∈
ℝ*) → 𝐷 ∈ (Clsd‘𝐽)) |
28 | 10, 12, 14, 27 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (Clsd‘𝐽)) |
29 | 13 | rpred 12772 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℝ) |
30 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (abs‘𝑦) = (abs‘𝑥)) |
31 | 30 | breq1d 5084 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((abs‘𝑦) ≤ 𝑅 ↔ (abs‘𝑥) ≤ 𝑅)) |
32 | 31, 1 | elrab2 3627 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) ≤ 𝑅)) |
33 | 32 | simprbi 497 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (abs‘𝑥) ≤ 𝑅) |
34 | 33 | rgen 3074 |
. . . . . . 7
⊢
∀𝑥 ∈
𝐷 (abs‘𝑥) ≤ 𝑅 |
35 | | brralrspcev 5134 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧
∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑅) → ∃𝑠 ∈ ℝ ∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑠) |
36 | 29, 34, 35 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → ∃𝑠 ∈ ℝ ∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑠) |
37 | | eqid 2738 |
. . . . . . . 8
⊢ (𝐽 ↾t 𝐷) = (𝐽 ↾t 𝐷) |
38 | 3, 37 | cnheibor 24118 |
. . . . . . 7
⊢ (𝐷 ⊆ ℂ → ((𝐽 ↾t 𝐷) ∈ Comp ↔ (𝐷 ∈ (Clsd‘𝐽) ∧ ∃𝑠 ∈ ℝ ∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑠))) |
39 | 2, 38 | ax-mp 5 |
. . . . . 6
⊢ ((𝐽 ↾t 𝐷) ∈ Comp ↔ (𝐷 ∈ (Clsd‘𝐽) ∧ ∃𝑠 ∈ ℝ ∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑠)) |
40 | 28, 36, 39 | sylanbrc 583 |
. . . . 5
⊢ (𝜑 → (𝐽 ↾t 𝐷) ∈ Comp) |
41 | | ftalem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
42 | | plycn 25422 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ (ℂ–cn→ℂ)) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) |
44 | | abscncf 24064 |
. . . . . . . . 9
⊢ abs
∈ (ℂ–cn→ℝ) |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → abs ∈
(ℂ–cn→ℝ)) |
46 | 43, 45 | cncfco 24070 |
. . . . . . 7
⊢ (𝜑 → (abs ∘ 𝐹) ∈ (ℂ–cn→ℝ)) |
47 | | ssid 3943 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
48 | | ax-resscn 10928 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
49 | 4 | toponrestid 22070 |
. . . . . . . . 9
⊢ 𝐽 = (𝐽 ↾t
ℂ) |
50 | 3 | tgioo2 23966 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (𝐽 ↾t
ℝ) |
51 | 3, 49, 50 | cncfcn 24073 |
. . . . . . . 8
⊢ ((ℂ
⊆ ℂ ∧ ℝ ⊆ ℂ) → (ℂ–cn→ℝ) = (𝐽 Cn (topGen‘ran
(,)))) |
52 | 47, 48, 51 | mp2an 689 |
. . . . . . 7
⊢
(ℂ–cn→ℝ) =
(𝐽 Cn (topGen‘ran
(,))) |
53 | 46, 52 | eleqtrdi 2849 |
. . . . . 6
⊢ (𝜑 → (abs ∘ 𝐹) ∈ (𝐽 Cn (topGen‘ran
(,)))) |
54 | 4 | toponunii 22065 |
. . . . . . 7
⊢ ℂ =
∪ 𝐽 |
55 | 54 | cnrest 22436 |
. . . . . 6
⊢ (((abs
∘ 𝐹) ∈ (𝐽 Cn (topGen‘ran (,)))
∧ 𝐷 ⊆ ℂ)
→ ((abs ∘ 𝐹)
↾ 𝐷) ∈ ((𝐽 ↾t 𝐷) Cn (topGen‘ran
(,)))) |
56 | 53, 2, 55 | sylancl 586 |
. . . . 5
⊢ (𝜑 → ((abs ∘ 𝐹) ↾ 𝐷) ∈ ((𝐽 ↾t 𝐷) Cn (topGen‘ran
(,)))) |
57 | 13 | rpge0d 12776 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑅) |
58 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (abs‘𝑦) =
(abs‘0)) |
59 | | abs0 14997 |
. . . . . . . . . 10
⊢
(abs‘0) = 0 |
60 | 58, 59 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (abs‘𝑦) = 0) |
61 | 60 | breq1d 5084 |
. . . . . . . 8
⊢ (𝑦 = 0 → ((abs‘𝑦) ≤ 𝑅 ↔ 0 ≤ 𝑅)) |
62 | 61, 1 | elrab2 3627 |
. . . . . . 7
⊢ (0 ∈
𝐷 ↔ (0 ∈ ℂ
∧ 0 ≤ 𝑅)) |
63 | 12, 57, 62 | sylanbrc 583 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐷) |
64 | 63 | ne0d 4269 |
. . . . 5
⊢ (𝜑 → 𝐷 ≠ ∅) |
65 | 7, 8, 40, 56, 64 | evth2 24123 |
. . . 4
⊢ (𝜑 → ∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥)) |
66 | | fvres 6793 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐷 → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = ((abs ∘ 𝐹)‘𝑧)) |
67 | 66 | ad2antlr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = ((abs ∘ 𝐹)‘𝑧)) |
68 | | plyf 25359 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
69 | 41, 68 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
70 | 69 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝐹:ℂ⟶ℂ) |
71 | | simplr 766 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑧 ∈ 𝐷) |
72 | 2, 71 | sselid 3919 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑧 ∈ ℂ) |
73 | | fvco3 6867 |
. . . . . . . . 9
⊢ ((𝐹:ℂ⟶ℂ ∧
𝑧 ∈ ℂ) →
((abs ∘ 𝐹)‘𝑧) = (abs‘(𝐹‘𝑧))) |
74 | 70, 72, 73 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((abs ∘ 𝐹)‘𝑧) = (abs‘(𝐹‘𝑧))) |
75 | 67, 74 | eqtrd 2778 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = (abs‘(𝐹‘𝑧))) |
76 | | fvres 6793 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = ((abs ∘ 𝐹)‘𝑥)) |
77 | 76 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = ((abs ∘ 𝐹)‘𝑥)) |
78 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
79 | 2, 78 | sselid 3919 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ) |
80 | | fvco3 6867 |
. . . . . . . . 9
⊢ ((𝐹:ℂ⟶ℂ ∧
𝑥 ∈ ℂ) →
((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹‘𝑥))) |
81 | 70, 79, 80 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹‘𝑥))) |
82 | 77, 81 | eqtrd 2778 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = (abs‘(𝐹‘𝑥))) |
83 | 75, 82 | breq12d 5087 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
84 | 83 | ralbidva 3111 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (∀𝑥 ∈ 𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
85 | 84 | rexbidva 3225 |
. . . 4
⊢ (𝜑 → (∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ ∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
86 | 65, 85 | mpbid 231 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |
87 | | ssrexv 3988 |
. . 3
⊢ (𝐷 ⊆ ℂ →
(∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → ∃𝑧 ∈ ℂ ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
88 | 2, 86, 87 | mpsyl 68 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ ℂ ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |
89 | 63 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 0 ∈ 𝐷) |
90 | | 2fveq3 6779 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘0))) |
91 | 90 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ↔ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)))) |
92 | 91 | rspcv 3557 |
. . . . . . 7
⊢ (0 ∈
𝐷 → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)))) |
93 | 89, 92 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)))) |
94 | 69 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝐹:ℂ⟶ℂ) |
95 | | ffvelrn 6959 |
. . . . . . . . . . 11
⊢ ((𝐹:ℂ⟶ℂ ∧ 0
∈ ℂ) → (𝐹‘0) ∈ ℂ) |
96 | 94, 11, 95 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹‘0) ∈ ℂ) |
97 | 96 | abscld 15148 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘0)) ∈ ℝ) |
98 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑥 ∈ (ℂ ∖ 𝐷)) |
99 | 98 | eldifad 3899 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑥 ∈ ℂ) |
100 | 94, 99 | ffvelrnd 6962 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹‘𝑥) ∈ ℂ) |
101 | 100 | abscld 15148 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
102 | | ftalem3.8 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ ℂ (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
103 | 102 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ∀𝑥 ∈ ℂ (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
104 | 98 | eldifbd 3900 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ¬ 𝑥 ∈ 𝐷) |
105 | 32 | baib 536 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ 𝐷 ↔ (abs‘𝑥) ≤ 𝑅)) |
106 | 99, 105 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝑥 ∈ 𝐷 ↔ (abs‘𝑥) ≤ 𝑅)) |
107 | 104, 106 | mtbid 324 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ¬ (abs‘𝑥) ≤ 𝑅) |
108 | 29 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑅 ∈ ℝ) |
109 | 99 | abscld 15148 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘𝑥) ∈ ℝ) |
110 | 108, 109 | ltnled 11122 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝑅 < (abs‘𝑥) ↔ ¬ (abs‘𝑥) ≤ 𝑅)) |
111 | 107, 110 | mpbird 256 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑅 < (abs‘𝑥)) |
112 | | rsp 3131 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ℂ (𝑅 <
(abs‘𝑥) →
(abs‘(𝐹‘0))
< (abs‘(𝐹‘𝑥))) → (𝑥 ∈ ℂ → (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))) |
113 | 103, 99, 111, 112 | syl3c 66 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))) |
114 | 97, 101, 113 | ltled 11123 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘0)) ≤ (abs‘(𝐹‘𝑥))) |
115 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑧 ∈ ℂ) |
116 | 94, 115 | ffvelrnd 6962 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹‘𝑧) ∈ ℂ) |
117 | 116 | abscld 15148 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
118 | | letr 11069 |
. . . . . . . . 9
⊢
(((abs‘(𝐹‘𝑧)) ∈ ℝ ∧ (abs‘(𝐹‘0)) ∈ ℝ ∧
(abs‘(𝐹‘𝑥)) ∈ ℝ) →
(((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)) ∧
(abs‘(𝐹‘0))
≤ (abs‘(𝐹‘𝑥))) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
119 | 117, 97, 101, 118 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)) ∧ (abs‘(𝐹‘0)) ≤
(abs‘(𝐹‘𝑥))) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
120 | 114, 119 | mpan2d 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
121 | 120 | ralrimdva 3106 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)) → ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
122 | 93, 121 | syld 47 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
123 | 122 | ancld 551 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))))) |
124 | | ralunb 4125 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐷 ∪ (ℂ ∖
𝐷))(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ↔ (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
125 | | undif2 4410 |
. . . . . . 7
⊢ (𝐷 ∪ (ℂ ∖ 𝐷)) = (𝐷 ∪ ℂ) |
126 | | ssequn1 4114 |
. . . . . . . 8
⊢ (𝐷 ⊆ ℂ ↔ (𝐷 ∪ ℂ) =
ℂ) |
127 | 2, 126 | mpbi 229 |
. . . . . . 7
⊢ (𝐷 ∪ ℂ) =
ℂ |
128 | 125, 127 | eqtri 2766 |
. . . . . 6
⊢ (𝐷 ∪ (ℂ ∖ 𝐷)) = ℂ |
129 | 128 | raleqi 3346 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐷 ∪ (ℂ ∖
𝐷))(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ↔ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |
130 | 124, 129 | bitr3i 276 |
. . . 4
⊢
((∀𝑥 ∈
𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) ↔ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |
131 | 123, 130 | syl6ib 250 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
132 | 131 | reximdva 3203 |
. 2
⊢ (𝜑 → (∃𝑧 ∈ ℂ ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → ∃𝑧 ∈ ℂ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
133 | 88, 132 | mpd 15 |
1
⊢ (𝜑 → ∃𝑧 ∈ ℂ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |