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