Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
(coeff‘(𝑧
∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) = (coeff‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) |
2 | | eqid 2610 |
. . . 4
⊢
(deg‘(𝑧 ∈
ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) = (deg‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) |
3 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
4 | | ftalem7.5 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑋 ∈ ℂ) |
6 | 3, 5 | addcld 9938 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧 + 𝑋) ∈ ℂ) |
7 | | cnex 9896 |
. . . . . . . . 9
⊢ ℂ
∈ V |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℂ ∈
V) |
9 | 4 | negcld 10258 |
. . . . . . . . 9
⊢ (𝜑 → -𝑋 ∈ ℂ) |
10 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → -𝑋 ∈ ℂ) |
11 | | df-idp 23749 |
. . . . . . . . . 10
⊢
Xp = ( I ↾ ℂ) |
12 | | mptresid 5375 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℂ ↦ 𝑧) = ( I ↾
ℂ) |
13 | 11, 12 | eqtr4i 2635 |
. . . . . . . . 9
⊢
Xp = (𝑧 ∈ ℂ ↦ 𝑧) |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → Xp =
(𝑧 ∈ ℂ ↦
𝑧)) |
15 | | fconstmpt 5085 |
. . . . . . . . 9
⊢ (ℂ
× {-𝑋}) = (𝑧 ∈ ℂ ↦ -𝑋) |
16 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℂ × {-𝑋}) = (𝑧 ∈ ℂ ↦ -𝑋)) |
17 | 8, 3, 10, 14, 16 | offval2 6812 |
. . . . . . 7
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {-𝑋})) = (𝑧 ∈ ℂ ↦ (𝑧 − -𝑋))) |
18 | | id 22 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℂ → 𝑧 ∈
ℂ) |
19 | | subneg 10209 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑧 − -𝑋) = (𝑧 + 𝑋)) |
20 | 18, 4, 19 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧 − -𝑋) = (𝑧 + 𝑋)) |
21 | 20 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (𝑧 − -𝑋)) = (𝑧 ∈ ℂ ↦ (𝑧 + 𝑋))) |
22 | 17, 21 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {-𝑋})) = (𝑧 ∈ ℂ ↦ (𝑧 + 𝑋))) |
23 | | ftalem.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
24 | | plyf 23758 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
26 | 25 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℂ ↦ (𝐹‘𝑦))) |
27 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = (𝑧 + 𝑋) → (𝐹‘𝑦) = (𝐹‘(𝑧 + 𝑋))) |
28 | 6, 22, 26, 27 | fmptco 6303 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘ (Xp
∘𝑓 − (ℂ × {-𝑋}))) = (𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) |
29 | | plyssc 23760 |
. . . . . . 7
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
30 | 29, 23 | sseldi 3566 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℂ)) |
31 | | eqid 2610 |
. . . . . . . . 9
⊢
(Xp ∘𝑓 − (ℂ
× {-𝑋})) =
(Xp ∘𝑓 − (ℂ ×
{-𝑋})) |
32 | 31 | plyremlem 23863 |
. . . . . . . 8
⊢ (-𝑋 ∈ ℂ →
((Xp ∘𝑓 − (ℂ ×
{-𝑋})) ∈
(Poly‘ℂ) ∧ (deg‘(Xp
∘𝑓 − (ℂ × {-𝑋}))) = 1 ∧ (◡(Xp
∘𝑓 − (ℂ × {-𝑋})) “ {0}) = {-𝑋})) |
33 | 9, 32 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {-𝑋})) ∈ (Poly‘ℂ) ∧
(deg‘(Xp ∘𝑓 − (ℂ
× {-𝑋}))) = 1 ∧
(◡(Xp
∘𝑓 − (ℂ × {-𝑋})) “ {0}) = {-𝑋})) |
34 | 33 | simp1d 1066 |
. . . . . 6
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {-𝑋})) ∈
(Poly‘ℂ)) |
35 | | addcl 9897 |
. . . . . . 7
⊢ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 + 𝑤) ∈ ℂ) |
36 | 35 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 + 𝑤) ∈ ℂ) |
37 | | mulcl 9899 |
. . . . . . 7
⊢ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 · 𝑤) ∈ ℂ) |
38 | 37 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ) |
39 | 30, 34, 36, 38 | plyco 23801 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘ (Xp
∘𝑓 − (ℂ × {-𝑋}))) ∈
(Poly‘ℂ)) |
40 | 28, 39 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))) ∈
(Poly‘ℂ)) |
41 | 28 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (deg‘(𝐹 ∘ (Xp
∘𝑓 − (ℂ × {-𝑋})))) = (deg‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))))) |
42 | | ftalem.2 |
. . . . . . 7
⊢ 𝑁 = (deg‘𝐹) |
43 | | eqid 2610 |
. . . . . . 7
⊢
(deg‘(Xp ∘𝑓 −
(ℂ × {-𝑋}))) =
(deg‘(Xp ∘𝑓 − (ℂ
× {-𝑋}))) |
44 | 42, 43, 30, 34 | dgrco 23835 |
. . . . . 6
⊢ (𝜑 → (deg‘(𝐹 ∘ (Xp
∘𝑓 − (ℂ × {-𝑋})))) = (𝑁 · (deg‘(Xp
∘𝑓 − (ℂ × {-𝑋}))))) |
45 | | ftalem.4 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
46 | 33 | simp2d 1067 |
. . . . . . . 8
⊢ (𝜑 →
(deg‘(Xp ∘𝑓 − (ℂ
× {-𝑋}))) =
1) |
47 | | 1nn 10908 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
48 | 46, 47 | syl6eqel 2696 |
. . . . . . 7
⊢ (𝜑 →
(deg‘(Xp ∘𝑓 − (ℂ
× {-𝑋}))) ∈
ℕ) |
49 | 45, 48 | nnmulcld 10945 |
. . . . . 6
⊢ (𝜑 → (𝑁 · (deg‘(Xp
∘𝑓 − (ℂ × {-𝑋})))) ∈ ℕ) |
50 | 44, 49 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → (deg‘(𝐹 ∘ (Xp
∘𝑓 − (ℂ × {-𝑋})))) ∈ ℕ) |
51 | 41, 50 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (deg‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) ∈ ℕ) |
52 | | 0cn 9911 |
. . . . . . 7
⊢ 0 ∈
ℂ |
53 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑧 = 0 → (𝑧 + 𝑋) = (0 + 𝑋)) |
54 | 53 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑧 = 0 → (𝐹‘(𝑧 + 𝑋)) = (𝐹‘(0 + 𝑋))) |
55 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))) = (𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))) |
56 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘(0 + 𝑋)) ∈ V |
57 | 54, 55, 56 | fvmpt 6191 |
. . . . . . 7
⊢ (0 ∈
ℂ → ((𝑧 ∈
ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) = (𝐹‘(0 + 𝑋))) |
58 | 52, 57 | ax-mp 5 |
. . . . . 6
⊢ ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) = (𝐹‘(0 + 𝑋)) |
59 | 4 | addid2d 10116 |
. . . . . . 7
⊢ (𝜑 → (0 + 𝑋) = 𝑋) |
60 | 59 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(0 + 𝑋)) = (𝐹‘𝑋)) |
61 | 58, 60 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) = (𝐹‘𝑋)) |
62 | | ftalem7.6 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑋) ≠ 0) |
63 | 61, 62 | eqnetrd 2849 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) ≠ 0) |
64 | 1, 2, 40, 51, 63 | ftalem6 24604 |
. . 3
⊢ (𝜑 → ∃𝑦 ∈ ℂ (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0))) |
65 | | id 22 |
. . . . . 6
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
66 | | addcl 9897 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑦 + 𝑋) ∈ ℂ) |
67 | 65, 4, 66 | syl2anr 494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 + 𝑋) ∈ ℂ) |
68 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑧 + 𝑋) = (𝑦 + 𝑋)) |
69 | 68 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (𝐹‘(𝑧 + 𝑋)) = (𝐹‘(𝑦 + 𝑋))) |
70 | | fvex 6113 |
. . . . . . . . . . 11
⊢ (𝐹‘(𝑦 + 𝑋)) ∈ V |
71 | 69, 55, 70 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦) = (𝐹‘(𝑦 + 𝑋))) |
72 | 71 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦) = (𝐹‘(𝑦 + 𝑋))) |
73 | 72 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) = (abs‘(𝐹‘(𝑦 + 𝑋)))) |
74 | 61 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) = (𝐹‘𝑋)) |
75 | 74 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) = (abs‘(𝐹‘𝑋))) |
76 | 73, 75 | breq12d 4596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) ↔ (abs‘(𝐹‘(𝑦 + 𝑋))) < (abs‘(𝐹‘𝑋)))) |
77 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐹:ℂ⟶ℂ) |
78 | 77, 67 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐹‘(𝑦 + 𝑋)) ∈ ℂ) |
79 | 78 | abscld 14023 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (abs‘(𝐹‘(𝑦 + 𝑋))) ∈ ℝ) |
80 | 25, 4 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑋) ∈ ℂ) |
81 | 80 | abscld 14023 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) ∈ ℝ) |
82 | 81 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (abs‘(𝐹‘𝑋)) ∈ ℝ) |
83 | 79, 82 | ltnled 10063 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((abs‘(𝐹‘(𝑦 + 𝑋))) < (abs‘(𝐹‘𝑋)) ↔ ¬ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋))))) |
84 | 76, 83 | bitrd 267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) ↔ ¬ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋))))) |
85 | 84 | biimpd 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) → ¬ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋))))) |
86 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 𝑋) → (𝐹‘𝑥) = (𝐹‘(𝑦 + 𝑋))) |
87 | 86 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 𝑋) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝑦 + 𝑋)))) |
88 | 87 | breq2d 4595 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 𝑋) → ((abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥)) ↔ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋))))) |
89 | 88 | notbid 307 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 𝑋) → (¬ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥)) ↔ ¬ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋))))) |
90 | 89 | rspcev 3282 |
. . . . 5
⊢ (((𝑦 + 𝑋) ∈ ℂ ∧ ¬
(abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋)))) → ∃𝑥 ∈ ℂ ¬ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥))) |
91 | 67, 85, 90 | syl6an 566 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) → ∃𝑥 ∈ ℂ ¬
(abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥)))) |
92 | 91 | rexlimdva 3013 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ℂ (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) → ∃𝑥 ∈ ℂ ¬
(abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥)))) |
93 | 64, 92 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℂ ¬ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥))) |
94 | | rexnal 2978 |
. 2
⊢
(∃𝑥 ∈
ℂ ¬ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥)) ↔ ¬ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥))) |
95 | 93, 94 | sylib 207 |
1
⊢ (𝜑 → ¬ ∀𝑥 ∈ ℂ
(abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥))) |