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 
|- ( ph -> F e. ( Poly ` S ) )
ftalem.4 
|- ( ph -> N e. NN )
ftalem7.5 
|- ( ph -> X e. CC )
ftalem7.6 
|- ( ph -> ( F ` X ) =/= 0 )
Assertion ftalem7 
|- ( ph -> -. A. x e. CC ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 
 |-  A = ( coeff ` F )
2 ftalem.2 
 |-  N = ( deg ` F )
3 ftalem.3 
 |-  ( ph -> F e. ( Poly ` S ) )
4 ftalem.4 
 |-  ( ph -> N e. NN )
5 ftalem7.5 
 |-  ( ph -> X e. CC )
6 ftalem7.6 
 |-  ( ph -> ( F ` X ) =/= 0 )
7 eqid 
 |-  ( coeff ` ( z e. CC |-> ( F ` ( z + X ) ) ) ) = ( coeff ` ( z e. CC |-> ( F ` ( z + X ) ) ) )
8 eqid 
 |-  ( deg ` ( z e. CC |-> ( F ` ( z + X ) ) ) ) = ( deg ` ( z e. CC |-> ( F ` ( z + X ) ) ) )
9 simpr 
 |-  ( ( ph /\ z e. CC ) -> z e. CC )
10 5 adantr 
 |-  ( ( ph /\ z e. CC ) -> X e. CC )
11 9 10 addcld 
 |-  ( ( ph /\ z e. CC ) -> ( z + X ) e. CC )
12 cnex 
 |-  CC e. _V
13 12 a1i 
 |-  ( ph -> CC e. _V )
14 5 negcld 
 |-  ( ph -> -u X e. CC )
15 14 adantr 
 |-  ( ( ph /\ z e. CC ) -> -u X e. CC )
16 df-idp 
 |-  Xp = ( _I |` CC )
17 mptresid 
 |-  ( _I |` CC ) = ( z e. CC |-> z )
18 16 17 eqtri 
 |-  Xp = ( z e. CC |-> z )
19 18 a1i 
 |-  ( ph -> Xp = ( z e. CC |-> z ) )
20 fconstmpt 
 |-  ( CC X. { -u X } ) = ( z e. CC |-> -u X )
21 20 a1i 
 |-  ( ph -> ( CC X. { -u X } ) = ( z e. CC |-> -u X ) )
22 13 9 15 19 21 offval2 
 |-  ( ph -> ( Xp oF - ( CC X. { -u X } ) ) = ( z e. CC |-> ( z - -u X ) ) )
23 id 
 |-  ( z e. CC -> z e. CC )
24 subneg 
 |-  ( ( z e. CC /\ X e. CC ) -> ( z - -u X ) = ( z + X ) )
25 23 5 24 syl2anr 
 |-  ( ( ph /\ z e. CC ) -> ( z - -u X ) = ( z + X ) )
26 25 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> ( z - -u X ) ) = ( z e. CC |-> ( z + X ) ) )
27 22 26 eqtrd 
 |-  ( ph -> ( Xp oF - ( CC X. { -u X } ) ) = ( z e. CC |-> ( z + X ) ) )
28 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
29 3 28 syl 
 |-  ( ph -> F : CC --> CC )
30 29 feqmptd 
 |-  ( ph -> F = ( y e. CC |-> ( F ` y ) ) )
31 fveq2 
 |-  ( y = ( z + X ) -> ( F ` y ) = ( F ` ( z + X ) ) )
32 11 27 30 31 fmptco 
 |-  ( ph -> ( F o. ( Xp oF - ( CC X. { -u X } ) ) ) = ( z e. CC |-> ( F ` ( z + X ) ) ) )
33 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
34 33 3 sselid 
 |-  ( ph -> F e. ( Poly ` CC ) )
35 eqid 
 |-  ( Xp oF - ( CC X. { -u X } ) ) = ( Xp oF - ( CC X. { -u X } ) )
36 35 plyremlem 
 |-  ( -u X e. CC -> ( ( Xp oF - ( CC X. { -u X } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { -u X } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { -u X } ) ) " { 0 } ) = { -u X } ) )
37 14 36 syl 
 |-  ( ph -> ( ( Xp oF - ( CC X. { -u X } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { -u X } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { -u X } ) ) " { 0 } ) = { -u X } ) )
38 37 simp1d 
 |-  ( ph -> ( Xp oF - ( CC X. { -u X } ) ) e. ( Poly ` CC ) )
39 addcl 
 |-  ( ( z e. CC /\ w e. CC ) -> ( z + w ) e. CC )
40 39 adantl 
 |-  ( ( ph /\ ( z e. CC /\ w e. CC ) ) -> ( z + w ) e. CC )
41 mulcl 
 |-  ( ( z e. CC /\ w e. CC ) -> ( z x. w ) e. CC )
42 41 adantl 
 |-  ( ( ph /\ ( z e. CC /\ w e. CC ) ) -> ( z x. w ) e. CC )
43 34 38 40 42 plyco 
 |-  ( ph -> ( F o. ( Xp oF - ( CC X. { -u X } ) ) ) e. ( Poly ` CC ) )
44 32 43 eqeltrrd 
 |-  ( ph -> ( z e. CC |-> ( F ` ( z + X ) ) ) e. ( Poly ` CC ) )
45 32 fveq2d 
 |-  ( ph -> ( deg ` ( F o. ( Xp oF - ( CC X. { -u X } ) ) ) ) = ( deg ` ( z e. CC |-> ( F ` ( z + X ) ) ) ) )
46 eqid 
 |-  ( deg ` ( Xp oF - ( CC X. { -u X } ) ) ) = ( deg ` ( Xp oF - ( CC X. { -u X } ) ) )
47 2 46 34 38 dgrco 
 |-  ( ph -> ( deg ` ( F o. ( Xp oF - ( CC X. { -u X } ) ) ) ) = ( N x. ( deg ` ( Xp oF - ( CC X. { -u X } ) ) ) ) )
48 37 simp2d 
 |-  ( ph -> ( deg ` ( Xp oF - ( CC X. { -u X } ) ) ) = 1 )
49 1nn 
 |-  1 e. NN
50 48 49 eqeltrdi 
 |-  ( ph -> ( deg ` ( Xp oF - ( CC X. { -u X } ) ) ) e. NN )
51 4 50 nnmulcld 
 |-  ( ph -> ( N x. ( deg ` ( Xp oF - ( CC X. { -u X } ) ) ) ) e. NN )
52 47 51 eqeltrd 
 |-  ( ph -> ( deg ` ( F o. ( Xp oF - ( CC X. { -u X } ) ) ) ) e. NN )
53 45 52 eqeltrrd 
 |-  ( ph -> ( deg ` ( z e. CC |-> ( F ` ( z + X ) ) ) ) e. NN )
54 0cn 
 |-  0 e. CC
55 fvoveq1 
 |-  ( z = 0 -> ( F ` ( z + X ) ) = ( F ` ( 0 + X ) ) )
56 eqid 
 |-  ( z e. CC |-> ( F ` ( z + X ) ) ) = ( z e. CC |-> ( F ` ( z + X ) ) )
57 fvex 
 |-  ( F ` ( 0 + X ) ) e. _V
58 55 56 57 fvmpt 
 |-  ( 0 e. CC -> ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) = ( F ` ( 0 + X ) ) )
59 54 58 ax-mp 
 |-  ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) = ( F ` ( 0 + X ) )
60 5 addid2d 
 |-  ( ph -> ( 0 + X ) = X )
61 60 fveq2d 
 |-  ( ph -> ( F ` ( 0 + X ) ) = ( F ` X ) )
62 59 61 syl5eq 
 |-  ( ph -> ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) = ( F ` X ) )
63 62 6 eqnetrd 
 |-  ( ph -> ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) =/= 0 )
64 7 8 44 53 63 ftalem6 
 |-  ( ph -> E. y e. CC ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) ) < ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) ) )
65 id 
 |-  ( y e. CC -> y e. CC )
66 addcl 
 |-  ( ( y e. CC /\ X e. CC ) -> ( y + X ) e. CC )
67 65 5 66 syl2anr 
 |-  ( ( ph /\ y e. CC ) -> ( y + X ) e. CC )
68 fvoveq1 
 |-  ( z = y -> ( F ` ( z + X ) ) = ( F ` ( y + X ) ) )
69 fvex 
 |-  ( F ` ( y + X ) ) e. _V
70 68 56 69 fvmpt 
 |-  ( y e. CC -> ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) = ( F ` ( y + X ) ) )
71 70 adantl 
 |-  ( ( ph /\ y e. CC ) -> ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) = ( F ` ( y + X ) ) )
72 71 fveq2d 
 |-  ( ( ph /\ y e. CC ) -> ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) ) = ( abs ` ( F ` ( y + X ) ) ) )
73 62 adantr 
 |-  ( ( ph /\ y e. CC ) -> ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) = ( F ` X ) )
74 73 fveq2d 
 |-  ( ( ph /\ y e. CC ) -> ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) ) = ( abs ` ( F ` X ) ) )
75 72 74 breq12d 
 |-  ( ( ph /\ y e. CC ) -> ( ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) ) < ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) ) <-> ( abs ` ( F ` ( y + X ) ) ) < ( abs ` ( F ` X ) ) ) )
76 29 adantr 
 |-  ( ( ph /\ y e. CC ) -> F : CC --> CC )
77 76 67 ffvelrnd 
 |-  ( ( ph /\ y e. CC ) -> ( F ` ( y + X ) ) e. CC )
78 77 abscld 
 |-  ( ( ph /\ y e. CC ) -> ( abs ` ( F ` ( y + X ) ) ) e. RR )
79 29 5 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. CC )
80 79 abscld 
 |-  ( ph -> ( abs ` ( F ` X ) ) e. RR )
81 80 adantr 
 |-  ( ( ph /\ y e. CC ) -> ( abs ` ( F ` X ) ) e. RR )
82 78 81 ltnled 
 |-  ( ( ph /\ y e. CC ) -> ( ( abs ` ( F ` ( y + X ) ) ) < ( abs ` ( F ` X ) ) <-> -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` ( y + X ) ) ) ) )
83 75 82 bitrd 
 |-  ( ( ph /\ y e. CC ) -> ( ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) ) < ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) ) <-> -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` ( y + X ) ) ) ) )
84 83 biimpd 
 |-  ( ( ph /\ y e. CC ) -> ( ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) ) < ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) ) -> -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` ( y + X ) ) ) ) )
85 2fveq3 
 |-  ( x = ( y + X ) -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` ( y + X ) ) ) )
86 85 breq2d 
 |-  ( x = ( y + X ) -> ( ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) <-> ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` ( y + X ) ) ) ) )
87 86 notbid 
 |-  ( x = ( y + X ) -> ( -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) <-> -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` ( y + X ) ) ) ) )
88 87 rspcev 
 |-  ( ( ( y + X ) e. CC /\ -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` ( y + X ) ) ) ) -> E. x e. CC -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) )
89 67 84 88 syl6an 
 |-  ( ( ph /\ y e. CC ) -> ( ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) ) < ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) ) -> E. x e. CC -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) ) )
90 89 rexlimdva 
 |-  ( ph -> ( E. y e. CC ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` y ) ) < ( abs ` ( ( z e. CC |-> ( F ` ( z + X ) ) ) ` 0 ) ) -> E. x e. CC -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) ) )
91 64 90 mpd 
 |-  ( ph -> E. x e. CC -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) )
92 rexnal 
 |-  ( E. x e. CC -. ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) <-> -. A. x e. CC ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) )
93 91 92 sylib 
 |-  ( ph -> -. A. x e. CC ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) )