Step | Hyp | Ref
| Expression |
1 | | ftalem3.5 |
. . . 4
⊢ 𝐷 = {𝑦 ∈ ℂ ∣ (abs‘𝑦) ≤ 𝑅} |
2 | 1 | ssrab3 3981 |
. . 3
⊢ 𝐷 ⊆
ℂ |
3 | | ftalem3.6 |
. . . . . . . 8
⊢ 𝐽 =
(TopOpen‘ℂfld) |
4 | 3 | cnfldtopon 23548 |
. . . . . . 7
⊢ 𝐽 ∈
(TopOn‘ℂ) |
5 | | resttopon 21925 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐷 ⊆ ℂ)
→ (𝐽
↾t 𝐷)
∈ (TopOn‘𝐷)) |
6 | 4, 2, 5 | mp2an 692 |
. . . . . 6
⊢ (𝐽 ↾t 𝐷) ∈ (TopOn‘𝐷) |
7 | 6 | toponunii 21680 |
. . . . 5
⊢ 𝐷 = ∪
(𝐽 ↾t
𝐷) |
8 | | eqid 2739 |
. . . . 5
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
9 | | cnxmet 23538 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
11 | | 0cn 10724 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℂ) |
13 | | ftalem3.7 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
14 | 13 | rpxrd 12528 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
15 | 3 | cnfldtopn 23547 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
16 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) |
17 | 16 | cnmetdval 23536 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℂ ∧ 𝑦
∈ ℂ) → (0(abs ∘ − )𝑦) = (abs‘(0 − 𝑦))) |
18 | 11, 17 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → (0(abs
∘ − )𝑦) =
(abs‘(0 − 𝑦))) |
19 | | df-neg 10964 |
. . . . . . . . . . . . . 14
⊢ -𝑦 = (0 − 𝑦) |
20 | 19 | fveq2i 6690 |
. . . . . . . . . . . . 13
⊢
(abs‘-𝑦) =
(abs‘(0 − 𝑦)) |
21 | | absneg 14740 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ →
(abs‘-𝑦) =
(abs‘𝑦)) |
22 | 20, 21 | eqtr3id 2788 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ →
(abs‘(0 − 𝑦)) =
(abs‘𝑦)) |
23 | 18, 22 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → (0(abs
∘ − )𝑦) =
(abs‘𝑦)) |
24 | 23 | breq1d 5050 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → ((0(abs
∘ − )𝑦) ≤
𝑅 ↔ (abs‘𝑦) ≤ 𝑅)) |
25 | 24 | rabbiia 3374 |
. . . . . . . . 9
⊢ {𝑦 ∈ ℂ ∣ (0(abs
∘ − )𝑦) ≤
𝑅} = {𝑦 ∈ ℂ ∣ (abs‘𝑦) ≤ 𝑅} |
26 | 1, 25 | eqtr4i 2765 |
. . . . . . . 8
⊢ 𝐷 = {𝑦 ∈ ℂ ∣ (0(abs ∘
− )𝑦) ≤ 𝑅} |
27 | 15, 26 | blcld 23271 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑅 ∈
ℝ*) → 𝐷 ∈ (Clsd‘𝐽)) |
28 | 10, 12, 14, 27 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (Clsd‘𝐽)) |
29 | 13 | rpred 12527 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℝ) |
30 | | fveq2 6687 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (abs‘𝑦) = (abs‘𝑥)) |
31 | 30 | breq1d 5050 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((abs‘𝑦) ≤ 𝑅 ↔ (abs‘𝑥) ≤ 𝑅)) |
32 | 31, 1 | elrab2 3596 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) ≤ 𝑅)) |
33 | 32 | simprbi 500 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (abs‘𝑥) ≤ 𝑅) |
34 | 33 | rgen 3064 |
. . . . . . 7
⊢
∀𝑥 ∈
𝐷 (abs‘𝑥) ≤ 𝑅 |
35 | | brralrspcev 5100 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧
∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑅) → ∃𝑠 ∈ ℝ ∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑠) |
36 | 29, 34, 35 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → ∃𝑠 ∈ ℝ ∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑠) |
37 | | eqid 2739 |
. . . . . . . 8
⊢ (𝐽 ↾t 𝐷) = (𝐽 ↾t 𝐷) |
38 | 3, 37 | cnheibor 23720 |
. . . . . . 7
⊢ (𝐷 ⊆ ℂ → ((𝐽 ↾t 𝐷) ∈ Comp ↔ (𝐷 ∈ (Clsd‘𝐽) ∧ ∃𝑠 ∈ ℝ ∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑠))) |
39 | 2, 38 | ax-mp 5 |
. . . . . 6
⊢ ((𝐽 ↾t 𝐷) ∈ Comp ↔ (𝐷 ∈ (Clsd‘𝐽) ∧ ∃𝑠 ∈ ℝ ∀𝑥 ∈ 𝐷 (abs‘𝑥) ≤ 𝑠)) |
40 | 28, 36, 39 | sylanbrc 586 |
. . . . 5
⊢ (𝜑 → (𝐽 ↾t 𝐷) ∈ Comp) |
41 | | ftalem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
42 | | plycn 25023 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ (ℂ–cn→ℂ)) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) |
44 | | abscncf 23666 |
. . . . . . . . 9
⊢ abs
∈ (ℂ–cn→ℝ) |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → abs ∈
(ℂ–cn→ℝ)) |
46 | 43, 45 | cncfco 23672 |
. . . . . . 7
⊢ (𝜑 → (abs ∘ 𝐹) ∈ (ℂ–cn→ℝ)) |
47 | | ssid 3909 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
48 | | ax-resscn 10685 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
49 | 4 | toponrestid 21685 |
. . . . . . . . 9
⊢ 𝐽 = (𝐽 ↾t
ℂ) |
50 | 3 | tgioo2 23568 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (𝐽 ↾t
ℝ) |
51 | 3, 49, 50 | cncfcn 23675 |
. . . . . . . 8
⊢ ((ℂ
⊆ ℂ ∧ ℝ ⊆ ℂ) → (ℂ–cn→ℝ) = (𝐽 Cn (topGen‘ran
(,)))) |
52 | 47, 48, 51 | mp2an 692 |
. . . . . . 7
⊢
(ℂ–cn→ℝ) =
(𝐽 Cn (topGen‘ran
(,))) |
53 | 46, 52 | eleqtrdi 2844 |
. . . . . 6
⊢ (𝜑 → (abs ∘ 𝐹) ∈ (𝐽 Cn (topGen‘ran
(,)))) |
54 | 4 | toponunii 21680 |
. . . . . . 7
⊢ ℂ =
∪ 𝐽 |
55 | 54 | cnrest 22049 |
. . . . . 6
⊢ (((abs
∘ 𝐹) ∈ (𝐽 Cn (topGen‘ran (,)))
∧ 𝐷 ⊆ ℂ)
→ ((abs ∘ 𝐹)
↾ 𝐷) ∈ ((𝐽 ↾t 𝐷) Cn (topGen‘ran
(,)))) |
56 | 53, 2, 55 | sylancl 589 |
. . . . 5
⊢ (𝜑 → ((abs ∘ 𝐹) ↾ 𝐷) ∈ ((𝐽 ↾t 𝐷) Cn (topGen‘ran
(,)))) |
57 | 13 | rpge0d 12531 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑅) |
58 | | fveq2 6687 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (abs‘𝑦) =
(abs‘0)) |
59 | | abs0 14748 |
. . . . . . . . . 10
⊢
(abs‘0) = 0 |
60 | 58, 59 | eqtrdi 2790 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (abs‘𝑦) = 0) |
61 | 60 | breq1d 5050 |
. . . . . . . 8
⊢ (𝑦 = 0 → ((abs‘𝑦) ≤ 𝑅 ↔ 0 ≤ 𝑅)) |
62 | 61, 1 | elrab2 3596 |
. . . . . . 7
⊢ (0 ∈
𝐷 ↔ (0 ∈ ℂ
∧ 0 ≤ 𝑅)) |
63 | 12, 57, 62 | sylanbrc 586 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐷) |
64 | 63 | ne0d 4234 |
. . . . 5
⊢ (𝜑 → 𝐷 ≠ ∅) |
65 | 7, 8, 40, 56, 64 | evth2 23725 |
. . . 4
⊢ (𝜑 → ∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥)) |
66 | | fvres 6706 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐷 → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = ((abs ∘ 𝐹)‘𝑧)) |
67 | 66 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = ((abs ∘ 𝐹)‘𝑧)) |
68 | | plyf 24960 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
69 | 41, 68 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
70 | 69 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝐹:ℂ⟶ℂ) |
71 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑧 ∈ 𝐷) |
72 | 2, 71 | sseldi 3885 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑧 ∈ ℂ) |
73 | | fvco3 6780 |
. . . . . . . . 9
⊢ ((𝐹:ℂ⟶ℂ ∧
𝑧 ∈ ℂ) →
((abs ∘ 𝐹)‘𝑧) = (abs‘(𝐹‘𝑧))) |
74 | 70, 72, 73 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((abs ∘ 𝐹)‘𝑧) = (abs‘(𝐹‘𝑧))) |
75 | 67, 74 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = (abs‘(𝐹‘𝑧))) |
76 | | fvres 6706 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = ((abs ∘ 𝐹)‘𝑥)) |
77 | 76 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = ((abs ∘ 𝐹)‘𝑥)) |
78 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
79 | 2, 78 | sseldi 3885 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ) |
80 | | fvco3 6780 |
. . . . . . . . 9
⊢ ((𝐹:ℂ⟶ℂ ∧
𝑥 ∈ ℂ) →
((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹‘𝑥))) |
81 | 70, 79, 80 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹‘𝑥))) |
82 | 77, 81 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = (abs‘(𝐹‘𝑥))) |
83 | 75, 82 | breq12d 5053 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
84 | 83 | ralbidva 3109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (∀𝑥 ∈ 𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
85 | 84 | rexbidva 3207 |
. . . 4
⊢ (𝜑 → (∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ ∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
86 | 65, 85 | mpbid 235 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |
87 | | ssrexv 3954 |
. . 3
⊢ (𝐷 ⊆ ℂ →
(∃𝑧 ∈ 𝐷 ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → ∃𝑧 ∈ ℂ ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
88 | 2, 86, 87 | mpsyl 68 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ ℂ ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |
89 | 63 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 0 ∈ 𝐷) |
90 | | 2fveq3 6692 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘0))) |
91 | 90 | breq2d 5052 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ↔ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)))) |
92 | 91 | rspcv 3524 |
. . . . . . 7
⊢ (0 ∈
𝐷 → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)))) |
93 | 89, 92 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)))) |
94 | 69 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝐹:ℂ⟶ℂ) |
95 | | ffvelrn 6872 |
. . . . . . . . . . 11
⊢ ((𝐹:ℂ⟶ℂ ∧ 0
∈ ℂ) → (𝐹‘0) ∈ ℂ) |
96 | 94, 11, 95 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹‘0) ∈ ℂ) |
97 | 96 | abscld 14899 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘0)) ∈ ℝ) |
98 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑥 ∈ (ℂ ∖ 𝐷)) |
99 | 98 | eldifad 3865 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑥 ∈ ℂ) |
100 | 94, 99 | ffvelrnd 6875 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹‘𝑥) ∈ ℂ) |
101 | 100 | abscld 14899 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
102 | | ftalem3.8 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ ℂ (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
103 | 102 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ∀𝑥 ∈ ℂ (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
104 | 98 | eldifbd 3866 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ¬ 𝑥 ∈ 𝐷) |
105 | 32 | baib 539 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ 𝐷 ↔ (abs‘𝑥) ≤ 𝑅)) |
106 | 99, 105 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝑥 ∈ 𝐷 ↔ (abs‘𝑥) ≤ 𝑅)) |
107 | 104, 106 | mtbid 327 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ¬ (abs‘𝑥) ≤ 𝑅) |
108 | 29 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑅 ∈ ℝ) |
109 | 99 | abscld 14899 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘𝑥) ∈ ℝ) |
110 | 108, 109 | ltnled 10878 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝑅 < (abs‘𝑥) ↔ ¬ (abs‘𝑥) ≤ 𝑅)) |
111 | 107, 110 | mpbird 260 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑅 < (abs‘𝑥)) |
112 | | rsp 3119 |
. . . . . . . . . 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 10879 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘0)) ≤ (abs‘(𝐹‘𝑥))) |
115 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑧 ∈ ℂ) |
116 | 94, 115 | ffvelrnd 6875 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹‘𝑧) ∈ ℂ) |
117 | 116 | abscld 14899 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
118 | | letr 10825 |
. . . . . . . . 9
⊢
(((abs‘(𝐹‘𝑧)) ∈ ℝ ∧ (abs‘(𝐹‘0)) ∈ ℝ ∧
(abs‘(𝐹‘𝑥)) ∈ ℝ) →
(((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)) ∧
(abs‘(𝐹‘0))
≤ (abs‘(𝐹‘𝑥))) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
119 | 117, 97, 101, 118 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)) ∧ (abs‘(𝐹‘0)) ≤
(abs‘(𝐹‘𝑥))) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
120 | 114, 119 | mpan2d 694 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)) → (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
121 | 120 | ralrimdva 3102 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘0)) → ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
122 | 93, 121 | syld 47 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
123 | 122 | ancld 554 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))))) |
124 | | ralunb 4091 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐷 ∪ (ℂ ∖
𝐷))(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ↔ (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
125 | | undif2 4376 |
. . . . . . 7
⊢ (𝐷 ∪ (ℂ ∖ 𝐷)) = (𝐷 ∪ ℂ) |
126 | | ssequn1 4080 |
. . . . . . . 8
⊢ (𝐷 ⊆ ℂ ↔ (𝐷 ∪ ℂ) =
ℂ) |
127 | 2, 126 | mpbi 233 |
. . . . . . 7
⊢ (𝐷 ∪ ℂ) =
ℂ |
128 | 125, 127 | eqtri 2762 |
. . . . . 6
⊢ (𝐷 ∪ (ℂ ∖ 𝐷)) = ℂ |
129 | 128 | raleqi 3315 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐷 ∪ (ℂ ∖
𝐷))(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ↔ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |
130 | 124, 129 | bitr3i 280 |
. . . 4
⊢
((∀𝑥 ∈
𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) ↔ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |
131 | 123, 130 | syl6ib 254 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
132 | 131 | reximdva 3185 |
. 2
⊢ (𝜑 → (∃𝑧 ∈ ℂ ∀𝑥 ∈ 𝐷 (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)) → ∃𝑧 ∈ ℂ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))) |
133 | 88, 132 | mpd 15 |
1
⊢ (𝜑 → ∃𝑧 ∈ ℂ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥))) |