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 ⊢ A = coeff ⁡ F
ftalem.2 ⊢ N = deg ⁡ F
ftalem.3 ⊢ φ → F ∈ Poly ⁡ S
ftalem.4 ⊢ φ → N ∈ ℕ
ftalem7.5 ⊢ φ → X ∈ ℂ
ftalem7.6 ⊢ φ → F ⁡ X ≠ 0
Assertion ftalem7 ⊢ φ → ¬ ∀ x ∈ ℂ F ⁡ X ≤ F ⁡ x

Proof

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