Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ftalem3 Structured version   Visualization version   GIF version

Theorem ftalem3 24846
 Description: Lemma for fta 24851. There exists a global minimum of the function abs ∘ 𝐹. The proof uses a circle of radius 𝑟 where 𝑟 is the value coming from ftalem1 24844; 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.)
Hypotheses
Ref Expression
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
Ref Expression
ftalem3 (𝜑 → ∃𝑧 ∈ ℂ ∀𝑥 ∈ ℂ (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑧,𝐷   𝑥,𝑁   𝑥,𝑦,𝐹,𝑧   𝑥,𝐽,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝑅,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑧)   𝐷(𝑦)   𝑅(𝑧)   𝑆(𝑥,𝑦,𝑧)   𝐽(𝑦)   𝑁(𝑦,𝑧)

Proof of Theorem ftalem3
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 ftalem3.5 . . . 4 𝐷 = {𝑦 ∈ ℂ ∣ (abs‘𝑦) ≤ 𝑅}
2 ssrab2 3720 . . . 4 {𝑦 ∈ ℂ ∣ (abs‘𝑦) ≤ 𝑅} ⊆ ℂ
31, 2eqsstri 3668 . . 3 𝐷 ⊆ ℂ
4 ftalem3.6 . . . . . . . 8 𝐽 = (TopOpen‘ℂfld)
54cnfldtopon 22633 . . . . . . 7 𝐽 ∈ (TopOn‘ℂ)
6 resttopon 21013 . . . . . . 7 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐷 ⊆ ℂ) → (𝐽t 𝐷) ∈ (TopOn‘𝐷))
75, 3, 6mp2an 708 . . . . . 6 (𝐽t 𝐷) ∈ (TopOn‘𝐷)
87toponunii 20769 . . . . 5 𝐷 = (𝐽t 𝐷)
9 eqid 2651 . . . . 5 (topGen‘ran (,)) = (topGen‘ran (,))
10 cnxmet 22623 . . . . . . . 8 (abs ∘ − ) ∈ (∞Met‘ℂ)
1110a1i 11 . . . . . . 7 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
12 0cn 10070 . . . . . . . 8 0 ∈ ℂ
1312a1i 11 . . . . . . 7 (𝜑 → 0 ∈ ℂ)
14 ftalem3.7 . . . . . . . 8 (𝜑𝑅 ∈ ℝ+)
1514rpxrd 11911 . . . . . . 7 (𝜑𝑅 ∈ ℝ*)
164cnfldtopn 22632 . . . . . . . 8 𝐽 = (MetOpen‘(abs ∘ − ))
17 eqid 2651 . . . . . . . . . . . . . 14 (abs ∘ − ) = (abs ∘ − )
1817cnmetdval 22621 . . . . . . . . . . . . 13 ((0 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0(abs ∘ − )𝑦) = (abs‘(0 − 𝑦)))
1912, 18mpan 706 . . . . . . . . . . . 12 (𝑦 ∈ ℂ → (0(abs ∘ − )𝑦) = (abs‘(0 − 𝑦)))
20 df-neg 10307 . . . . . . . . . . . . . 14 -𝑦 = (0 − 𝑦)
2120fveq2i 6232 . . . . . . . . . . . . 13 (abs‘-𝑦) = (abs‘(0 − 𝑦))
22 absneg 14061 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → (abs‘-𝑦) = (abs‘𝑦))
2321, 22syl5eqr 2699 . . . . . . . . . . . 12 (𝑦 ∈ ℂ → (abs‘(0 − 𝑦)) = (abs‘𝑦))
2419, 23eqtrd 2685 . . . . . . . . . . 11 (𝑦 ∈ ℂ → (0(abs ∘ − )𝑦) = (abs‘𝑦))
2524breq1d 4695 . . . . . . . . . 10 (𝑦 ∈ ℂ → ((0(abs ∘ − )𝑦) ≤ 𝑅 ↔ (abs‘𝑦) ≤ 𝑅))
2625rabbiia 3215 . . . . . . . . 9 {𝑦 ∈ ℂ ∣ (0(abs ∘ − )𝑦) ≤ 𝑅} = {𝑦 ∈ ℂ ∣ (abs‘𝑦) ≤ 𝑅}
271, 26eqtr4i 2676 . . . . . . . 8 𝐷 = {𝑦 ∈ ℂ ∣ (0(abs ∘ − )𝑦) ≤ 𝑅}
2816, 27blcld 22357 . . . . . . 7 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → 𝐷 ∈ (Clsd‘𝐽))
2911, 13, 15, 28syl3anc 1366 . . . . . 6 (𝜑𝐷 ∈ (Clsd‘𝐽))
3014rpred 11910 . . . . . . 7 (𝜑𝑅 ∈ ℝ)
31 fveq2 6229 . . . . . . . . . . 11 (𝑦 = 𝑥 → (abs‘𝑦) = (abs‘𝑥))
3231breq1d 4695 . . . . . . . . . 10 (𝑦 = 𝑥 → ((abs‘𝑦) ≤ 𝑅 ↔ (abs‘𝑥) ≤ 𝑅))
3332, 1elrab2 3399 . . . . . . . . 9 (𝑥𝐷 ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) ≤ 𝑅))
3433simprbi 479 . . . . . . . 8 (𝑥𝐷 → (abs‘𝑥) ≤ 𝑅)
3534rgen 2951 . . . . . . 7 𝑥𝐷 (abs‘𝑥) ≤ 𝑅
36 breq2 4689 . . . . . . . . 9 (𝑠 = 𝑅 → ((abs‘𝑥) ≤ 𝑠 ↔ (abs‘𝑥) ≤ 𝑅))
3736ralbidv 3015 . . . . . . . 8 (𝑠 = 𝑅 → (∀𝑥𝐷 (abs‘𝑥) ≤ 𝑠 ↔ ∀𝑥𝐷 (abs‘𝑥) ≤ 𝑅))
3837rspcev 3340 . . . . . . 7 ((𝑅 ∈ ℝ ∧ ∀𝑥𝐷 (abs‘𝑥) ≤ 𝑅) → ∃𝑠 ∈ ℝ ∀𝑥𝐷 (abs‘𝑥) ≤ 𝑠)
3930, 35, 38sylancl 695 . . . . . 6 (𝜑 → ∃𝑠 ∈ ℝ ∀𝑥𝐷 (abs‘𝑥) ≤ 𝑠)
40 eqid 2651 . . . . . . . 8 (𝐽t 𝐷) = (𝐽t 𝐷)
414, 40cnheibor 22801 . . . . . . 7 (𝐷 ⊆ ℂ → ((𝐽t 𝐷) ∈ Comp ↔ (𝐷 ∈ (Clsd‘𝐽) ∧ ∃𝑠 ∈ ℝ ∀𝑥𝐷 (abs‘𝑥) ≤ 𝑠)))
423, 41ax-mp 5 . . . . . 6 ((𝐽t 𝐷) ∈ Comp ↔ (𝐷 ∈ (Clsd‘𝐽) ∧ ∃𝑠 ∈ ℝ ∀𝑥𝐷 (abs‘𝑥) ≤ 𝑠))
4329, 39, 42sylanbrc 699 . . . . 5 (𝜑 → (𝐽t 𝐷) ∈ Comp)
44 ftalem.3 . . . . . . . . 9 (𝜑𝐹 ∈ (Poly‘𝑆))
45 plycn 24062 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ (ℂ–cn→ℂ))
4644, 45syl 17 . . . . . . . 8 (𝜑𝐹 ∈ (ℂ–cn→ℂ))
47 abscncf 22751 . . . . . . . . 9 abs ∈ (ℂ–cn→ℝ)
4847a1i 11 . . . . . . . 8 (𝜑 → abs ∈ (ℂ–cn→ℝ))
4946, 48cncfco 22757 . . . . . . 7 (𝜑 → (abs ∘ 𝐹) ∈ (ℂ–cn→ℝ))
50 ssid 3657 . . . . . . . 8 ℂ ⊆ ℂ
51 ax-resscn 10031 . . . . . . . 8 ℝ ⊆ ℂ
524cnfldtop 22634 . . . . . . . . . . 11 𝐽 ∈ Top
535toponunii 20769 . . . . . . . . . . . 12 ℂ = 𝐽
5453restid 16141 . . . . . . . . . . 11 (𝐽 ∈ Top → (𝐽t ℂ) = 𝐽)
5552, 54ax-mp 5 . . . . . . . . . 10 (𝐽t ℂ) = 𝐽
5655eqcomi 2660 . . . . . . . . 9 𝐽 = (𝐽t ℂ)
574tgioo2 22653 . . . . . . . . 9 (topGen‘ran (,)) = (𝐽t ℝ)
584, 56, 57cncfcn 22759 . . . . . . . 8 ((ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (ℂ–cn→ℝ) = (𝐽 Cn (topGen‘ran (,))))
5950, 51, 58mp2an 708 . . . . . . 7 (ℂ–cn→ℝ) = (𝐽 Cn (topGen‘ran (,)))
6049, 59syl6eleq 2740 . . . . . 6 (𝜑 → (abs ∘ 𝐹) ∈ (𝐽 Cn (topGen‘ran (,))))
6153cnrest 21137 . . . . . 6 (((abs ∘ 𝐹) ∈ (𝐽 Cn (topGen‘ran (,))) ∧ 𝐷 ⊆ ℂ) → ((abs ∘ 𝐹) ↾ 𝐷) ∈ ((𝐽t 𝐷) Cn (topGen‘ran (,))))
6260, 3, 61sylancl 695 . . . . 5 (𝜑 → ((abs ∘ 𝐹) ↾ 𝐷) ∈ ((𝐽t 𝐷) Cn (topGen‘ran (,))))
6314rpge0d 11914 . . . . . . 7 (𝜑 → 0 ≤ 𝑅)
64 fveq2 6229 . . . . . . . . . 10 (𝑦 = 0 → (abs‘𝑦) = (abs‘0))
65 abs0 14069 . . . . . . . . . 10 (abs‘0) = 0
6664, 65syl6eq 2701 . . . . . . . . 9 (𝑦 = 0 → (abs‘𝑦) = 0)
6766breq1d 4695 . . . . . . . 8 (𝑦 = 0 → ((abs‘𝑦) ≤ 𝑅 ↔ 0 ≤ 𝑅))
6867, 1elrab2 3399 . . . . . . 7 (0 ∈ 𝐷 ↔ (0 ∈ ℂ ∧ 0 ≤ 𝑅))
6913, 63, 68sylanbrc 699 . . . . . 6 (𝜑 → 0 ∈ 𝐷)
70 ne0i 3954 . . . . . 6 (0 ∈ 𝐷𝐷 ≠ ∅)
7169, 70syl 17 . . . . 5 (𝜑𝐷 ≠ ∅)
728, 9, 43, 62, 71evth2 22806 . . . 4 (𝜑 → ∃𝑧𝐷𝑥𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥))
73 fvres 6245 . . . . . . . . 9 (𝑧𝐷 → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = ((abs ∘ 𝐹)‘𝑧))
7473ad2antlr 763 . . . . . . . 8 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = ((abs ∘ 𝐹)‘𝑧))
75 plyf 23999 . . . . . . . . . . 11 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
7644, 75syl 17 . . . . . . . . . 10 (𝜑𝐹:ℂ⟶ℂ)
7776ad2antrr 762 . . . . . . . . 9 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → 𝐹:ℂ⟶ℂ)
78 simplr 807 . . . . . . . . . 10 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → 𝑧𝐷)
793, 78sseldi 3634 . . . . . . . . 9 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → 𝑧 ∈ ℂ)
80 fvco3 6314 . . . . . . . . 9 ((𝐹:ℂ⟶ℂ ∧ 𝑧 ∈ ℂ) → ((abs ∘ 𝐹)‘𝑧) = (abs‘(𝐹𝑧)))
8177, 79, 80syl2anc 694 . . . . . . . 8 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → ((abs ∘ 𝐹)‘𝑧) = (abs‘(𝐹𝑧)))
8274, 81eqtrd 2685 . . . . . . 7 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) = (abs‘(𝐹𝑧)))
83 fvres 6245 . . . . . . . . 9 (𝑥𝐷 → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = ((abs ∘ 𝐹)‘𝑥))
8483adantl 481 . . . . . . . 8 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = ((abs ∘ 𝐹)‘𝑥))
85 simpr 476 . . . . . . . . . 10 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → 𝑥𝐷)
863, 85sseldi 3634 . . . . . . . . 9 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → 𝑥 ∈ ℂ)
87 fvco3 6314 . . . . . . . . 9 ((𝐹:ℂ⟶ℂ ∧ 𝑥 ∈ ℂ) → ((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹𝑥)))
8877, 86, 87syl2anc 694 . . . . . . . 8 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → ((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹𝑥)))
8984, 88eqtrd 2685 . . . . . . 7 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) = (abs‘(𝐹𝑥)))
9082, 89breq12d 4698 . . . . . 6 (((𝜑𝑧𝐷) ∧ 𝑥𝐷) → ((((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
9190ralbidva 3014 . . . . 5 ((𝜑𝑧𝐷) → (∀𝑥𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ ∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
9291rexbidva 3078 . . . 4 (𝜑 → (∃𝑧𝐷𝑥𝐷 (((abs ∘ 𝐹) ↾ 𝐷)‘𝑧) ≤ (((abs ∘ 𝐹) ↾ 𝐷)‘𝑥) ↔ ∃𝑧𝐷𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
9372, 92mpbid 222 . . 3 (𝜑 → ∃𝑧𝐷𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)))
94 ssrexv 3700 . . 3 (𝐷 ⊆ ℂ → (∃𝑧𝐷𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) → ∃𝑧 ∈ ℂ ∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
953, 93, 94mpsyl 68 . 2 (𝜑 → ∃𝑧 ∈ ℂ ∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)))
9669adantr 480 . . . . . . 7 ((𝜑𝑧 ∈ ℂ) → 0 ∈ 𝐷)
97 fveq2 6229 . . . . . . . . . 10 (𝑥 = 0 → (𝐹𝑥) = (𝐹‘0))
9897fveq2d 6233 . . . . . . . . 9 (𝑥 = 0 → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘0)))
9998breq2d 4697 . . . . . . . 8 (𝑥 = 0 → ((abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) ↔ (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹‘0))))
10099rspcv 3336 . . . . . . 7 (0 ∈ 𝐷 → (∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) → (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹‘0))))
10196, 100syl 17 . . . . . 6 ((𝜑𝑧 ∈ ℂ) → (∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) → (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹‘0))))
10276ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝐹:ℂ⟶ℂ)
103 ffvelrn 6397 . . . . . . . . . . 11 ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
104102, 12, 103sylancl 695 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹‘0) ∈ ℂ)
105104abscld 14219 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘0)) ∈ ℝ)
106 simpr 476 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑥 ∈ (ℂ ∖ 𝐷))
107106eldifad 3619 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑥 ∈ ℂ)
108102, 107ffvelrnd 6400 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹𝑥) ∈ ℂ)
109108abscld 14219 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹𝑥)) ∈ ℝ)
110 ftalem3.8 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ ℂ (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
111110ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ∀𝑥 ∈ ℂ (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
112106eldifbd 3620 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ¬ 𝑥𝐷)
11333baib 964 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (𝑥𝐷 ↔ (abs‘𝑥) ≤ 𝑅))
114107, 113syl 17 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝑥𝐷 ↔ (abs‘𝑥) ≤ 𝑅))
115112, 114mtbid 313 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ¬ (abs‘𝑥) ≤ 𝑅)
11630ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑅 ∈ ℝ)
117107abscld 14219 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘𝑥) ∈ ℝ)
118116, 117ltnled 10222 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝑅 < (abs‘𝑥) ↔ ¬ (abs‘𝑥) ≤ 𝑅))
119115, 118mpbird 247 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑅 < (abs‘𝑥))
120 rsp 2958 . . . . . . . . . 10 (∀𝑥 ∈ ℂ (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))) → (𝑥 ∈ ℂ → (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
121111, 107, 119, 120syl3c 66 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))
122105, 109, 121ltled 10223 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹‘0)) ≤ (abs‘(𝐹𝑥)))
123 simplr 807 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → 𝑧 ∈ ℂ)
124102, 123ffvelrnd 6400 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (𝐹𝑧) ∈ ℂ)
125124abscld 14219 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (abs‘(𝐹𝑧)) ∈ ℝ)
126 letr 10169 . . . . . . . . 9 (((abs‘(𝐹𝑧)) ∈ ℝ ∧ (abs‘(𝐹‘0)) ∈ ℝ ∧ (abs‘(𝐹𝑥)) ∈ ℝ) → (((abs‘(𝐹𝑧)) ≤ (abs‘(𝐹‘0)) ∧ (abs‘(𝐹‘0)) ≤ (abs‘(𝐹𝑥))) → (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
127125, 105, 109, 126syl3anc 1366 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → (((abs‘(𝐹𝑧)) ≤ (abs‘(𝐹‘0)) ∧ (abs‘(𝐹‘0)) ≤ (abs‘(𝐹𝑥))) → (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
128122, 127mpan2d 710 . . . . . . 7 (((𝜑𝑧 ∈ ℂ) ∧ 𝑥 ∈ (ℂ ∖ 𝐷)) → ((abs‘(𝐹𝑧)) ≤ (abs‘(𝐹‘0)) → (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
129128ralrimdva 2998 . . . . . 6 ((𝜑𝑧 ∈ ℂ) → ((abs‘(𝐹𝑧)) ≤ (abs‘(𝐹‘0)) → ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
130101, 129syld 47 . . . . 5 ((𝜑𝑧 ∈ ℂ) → (∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) → ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
131130ancld 575 . . . 4 ((𝜑𝑧 ∈ ℂ) → (∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) → (∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)))))
132 ralunb 3827 . . . . 5 (∀𝑥 ∈ (𝐷 ∪ (ℂ ∖ 𝐷))(abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) ↔ (∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
133 undif2 4077 . . . . . . 7 (𝐷 ∪ (ℂ ∖ 𝐷)) = (𝐷 ∪ ℂ)
134 ssequn1 3816 . . . . . . . 8 (𝐷 ⊆ ℂ ↔ (𝐷 ∪ ℂ) = ℂ)
1353, 134mpbi 220 . . . . . . 7 (𝐷 ∪ ℂ) = ℂ
136133, 135eqtri 2673 . . . . . 6 (𝐷 ∪ (ℂ ∖ 𝐷)) = ℂ
137136raleqi 3172 . . . . 5 (∀𝑥 ∈ (𝐷 ∪ (ℂ ∖ 𝐷))(abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) ↔ ∀𝑥 ∈ ℂ (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)))
138132, 137bitr3i 266 . . . 4 ((∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) ∧ ∀𝑥 ∈ (ℂ ∖ 𝐷)(abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))) ↔ ∀𝑥 ∈ ℂ (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)))
139131, 138syl6ib 241 . . 3 ((𝜑𝑧 ∈ ℂ) → (∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) → ∀𝑥 ∈ ℂ (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
140139reximdva 3046 . 2 (𝜑 → (∃𝑧 ∈ ℂ ∀𝑥𝐷 (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)) → ∃𝑧 ∈ ℂ ∀𝑥 ∈ ℂ (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥))))
14195, 140mpd 15 1 (𝜑 → ∃𝑧 ∈ ℂ ∀𝑥 ∈ ℂ (abs‘(𝐹𝑧)) ≤ (abs‘(𝐹𝑥)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945   ∖ cdif 3604   ∪ cun 3605   ⊆ wss 3607  ∅c0 3948   class class class wbr 4685  ran crn 5144   ↾ cres 5145   ∘ ccom 5147  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305  ℕcn 11058  ℝ+crp 11870  (,)cioo 12213  abscabs 14018   ↾t crest 16128  TopOpenctopn 16129  topGenctg 16145  ∞Metcxmt 19779  ℂfldccnfld 19794  Topctop 20746  TopOnctopon 20763  Clsdccld 20868   Cn ccn 21076  Compccmp 21237  –cn→ccncf 22726  Polycply 23985  coeffccoe 23987  degcdgr 23988 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-cls 20873  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-0p 23482  df-ply 23989  df-coe 23991  df-dgr 23992 This theorem is referenced by:  fta  24851
 Copyright terms: Public domain W3C validator