Metamath Proof Explorer

Theorem ftalem7

Description: Lemma for fta . Shift the minimum away from zero by a change of variables. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ftalem7.5 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
ftalem7.6 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≠ 0 )
Assertion ftalem7 ( 𝜑 → ¬ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4 ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5 ftalem7.5 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
6 ftalem7.6 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≠ 0 )
7 eqid ⊢ ( coeff ‘ ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ) = ( coeff ‘ ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) )
8 eqid ⊢ ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ) = ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
10 5 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑋 ∈ ℂ )
11 9 10 addcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝑧 + 𝑋 ) ∈ ℂ )
12 cnex ⊢ ℂ ∈ V
13 12 a1i ⊢ ( 𝜑 → ℂ ∈ V )
14 5 negcld ⊢ ( 𝜑 → - 𝑋 ∈ ℂ )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → - 𝑋 ∈ ℂ )
16 df-idp ⊢ Xp = ( I ↾ ℂ )
17 mptresid ⊢ ( I ↾ ℂ ) = ( 𝑧 ∈ ℂ ↦ 𝑧 )
18 16 17 eqtri ⊢ Xp = ( 𝑧 ∈ ℂ ↦ 𝑧 )
19 18 a1i ⊢ ( 𝜑 → Xp = ( 𝑧 ∈ ℂ ↦ 𝑧 ) )
20 fconstmpt ⊢ ( ℂ × { - 𝑋 } ) = ( 𝑧 ∈ ℂ ↦ - 𝑋 )
21 20 a1i ⊢ ( 𝜑 → ( ℂ × { - 𝑋 } ) = ( 𝑧 ∈ ℂ ↦ - 𝑋 ) )
22 13 9 15 19 21 offval2 ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 − - 𝑋 ) ) )
23 id ⊢ ( 𝑧 ∈ ℂ → 𝑧 ∈ ℂ )
24 subneg ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝑧 − - 𝑋 ) = ( 𝑧 + 𝑋 ) )
25 23 5 24 syl2anr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝑧 − - 𝑋 ) = ( 𝑧 + 𝑋 ) )
26 25 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ ( 𝑧 − - 𝑋 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 + 𝑋 ) ) )
27 22 26 eqtrd ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 + 𝑋 ) ) )
28 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
29 3 28 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
30 29 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℂ ↦ ( 𝐹 ‘ 𝑦 ) ) )
31 fveq2 ⊢ ( 𝑦 = ( 𝑧 + 𝑋 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) )
32 11 27 30 31 fmptco ⊢ ( 𝜑 → ( 𝐹 ∘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) )
33 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
34 33 3 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℂ ) )
35 eqid ⊢ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) = ( Xp ∘f − ( ℂ × { - 𝑋 } ) )
36 35 plyremlem ⊢ ( - 𝑋 ∈ ℂ → ( ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) “ { 0 } ) = { - 𝑋 } ) )
37 14 36 syl ⊢ ( 𝜑 → ( ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) “ { 0 } ) = { - 𝑋 } ) )
38 37 simp1d ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ∈ ( Poly ‘ ℂ ) )
39 addcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑧 + 𝑤 ) ∈ ℂ )
40 39 adantl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( 𝑧 + 𝑤 ) ∈ ℂ )
41 mulcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑧 · 𝑤 ) ∈ ℂ )
42 41 adantl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( 𝑧 · 𝑤 ) ∈ ℂ )
43 34 38 40 42 plyco ⊢ ( 𝜑 → ( 𝐹 ∘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) ∈ ( Poly ‘ ℂ ) )
44 32 43 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ∈ ( Poly ‘ ℂ ) )
45 32 fveq2d ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) ) = ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ) )
46 eqid ⊢ ( deg ‘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) = ( deg ‘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) )
47 2 46 34 38 dgrco ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) ) = ( 𝑁 · ( deg ‘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) ) )
48 37 simp2d ⊢ ( 𝜑 → ( deg ‘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) = 1 )
49 1nn ⊢ 1 ∈ ℕ
50 48 49 eqeltrdi ⊢ ( 𝜑 → ( deg ‘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) ∈ ℕ )
51 4 50 nnmulcld ⊢ ( 𝜑 → ( 𝑁 · ( deg ‘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) ) ∈ ℕ )
52 47 51 eqeltrd ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘ ( Xp ∘f − ( ℂ × { - 𝑋 } ) ) ) ) ∈ ℕ )
53 45 52 eqeltrrd ⊢ ( 𝜑 → ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ) ∈ ℕ )
54 0cn ⊢ 0 ∈ ℂ
55 fvoveq1 ⊢ ( 𝑧 = 0 → ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) = ( 𝐹 ‘ ( 0 + 𝑋 ) ) )
56 eqid ⊢ ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) )
57 fvex ⊢ ( 𝐹 ‘ ( 0 + 𝑋 ) ) ∈ V
58 55 56 57 fvmpt ⊢ ( 0 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) = ( 𝐹 ‘ ( 0 + 𝑋 ) ) )
59 54 58 ax-mp ⊢ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) = ( 𝐹 ‘ ( 0 + 𝑋 ) )
60 5 addlidd ⊢ ( 𝜑 → ( 0 + 𝑋 ) = 𝑋 )
61 60 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0 + 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
62 59 61 eqtrid ⊢ ( 𝜑 → ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) = ( 𝐹 ‘ 𝑋 ) )
63 62 6 eqnetrd ⊢ ( 𝜑 → ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) ≠ 0 )
64 7 8 44 53 63 ftalem6 ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℂ ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) ) < ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) ) )
65 id ⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ )
66 addcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝑦 + 𝑋 ) ∈ ℂ )
67 65 5 66 syl2anr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 + 𝑋 ) ∈ ℂ )
68 fvoveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) )
69 fvex ⊢ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ∈ V
70 68 56 69 fvmpt ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) )
72 71 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) )
73 62 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) = ( 𝐹 ‘ 𝑋 ) )
74 73 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) )
75 72 74 breq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) ) < ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) ) ↔ ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) < ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
76 29 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐹 : ℂ ⟶ ℂ )
77 76 67 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ∈ ℂ )
78 77 abscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) ∈ ℝ )
79 29 5 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℂ )
80 79 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
82 78 81 ltnled ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) < ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ↔ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) ) )
83 75 82 bitrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) ) < ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) ) ↔ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) ) )
84 83 biimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) ) < ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) ) → ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) ) )
85 2fveq3 ⊢ ( 𝑥 = ( 𝑦 + 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) )
86 85 breq2d ⊢ ( 𝑥 = ( 𝑦 + 𝑋 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) ) )
87 86 notbid ⊢ ( 𝑥 = ( 𝑦 + 𝑋 ) → ( ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) ) )
88 87 rspcev ⊢ ( ( ( 𝑦 + 𝑋 ) ∈ ℂ ∧ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑦 + 𝑋 ) ) ) ) → ∃ 𝑥 ∈ ℂ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
89 67 84 88 syl6an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) ) < ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) ) → ∃ 𝑥 ∈ ℂ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
90 89 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℂ ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 𝑦 ) ) < ( abs ‘ ( ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝑧 + 𝑋 ) ) ) ‘ 0 ) ) → ∃ 𝑥 ∈ ℂ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
91 64 90 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℂ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
92 rexnal ⊢ ( ∃ 𝑥 ∈ ℂ ¬ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ¬ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
93 91 92 sylib ⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )