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 ) ) )