Metamath Proof Explorer


Theorem signsply0

Description: Lemma for the rule of signs, based on Bolzano's intermediate value theorem for polynomials : If the lowest and highest coefficient A and B are of opposite signs, the polynomial admits a positive root. (Contributed by Thierry Arnoux, 19-Sep-2018)

Ref Expression
Hypotheses signsply0.d
|- D = ( deg ` F )
signsply0.c
|- C = ( coeff ` F )
signsply0.b
|- B = ( C ` D )
signsply0.a
|- A = ( C ` 0 )
signsply0.1
|- ( ph -> F e. ( Poly ` RR ) )
signsply0.2
|- ( ph -> F =/= 0p )
signsply0.3
|- ( ph -> ( A x. B ) < 0 )
Assertion signsply0
|- ( ph -> E. z e. RR+ ( F ` z ) = 0 )

Proof

Step Hyp Ref Expression
1 signsply0.d
 |-  D = ( deg ` F )
2 signsply0.c
 |-  C = ( coeff ` F )
3 signsply0.b
 |-  B = ( C ` D )
4 signsply0.a
 |-  A = ( C ` 0 )
5 signsply0.1
 |-  ( ph -> F e. ( Poly ` RR ) )
6 signsply0.2
 |-  ( ph -> F =/= 0p )
7 signsply0.3
 |-  ( ph -> ( A x. B ) < 0 )
8 simplr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) -> d e. RR+ )
9 simpr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) -> A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) )
10 rpxr
 |-  ( d e. RR+ -> d e. RR* )
11 10 xrleidd
 |-  ( d e. RR+ -> d <_ d )
12 11 ad2antlr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) -> d <_ d )
13 id
 |-  ( d e. RR+ -> d e. RR+ )
14 simpr
 |-  ( ( d e. RR+ /\ f = d ) -> f = d )
15 14 breq2d
 |-  ( ( d e. RR+ /\ f = d ) -> ( d <_ f <-> d <_ d ) )
16 14 fveq2d
 |-  ( ( d e. RR+ /\ f = d ) -> ( F ` f ) = ( F ` d ) )
17 14 oveq1d
 |-  ( ( d e. RR+ /\ f = d ) -> ( f ^ D ) = ( d ^ D ) )
18 16 17 oveq12d
 |-  ( ( d e. RR+ /\ f = d ) -> ( ( F ` f ) / ( f ^ D ) ) = ( ( F ` d ) / ( d ^ D ) ) )
19 18 fvoveq1d
 |-  ( ( d e. RR+ /\ f = d ) -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) = ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) )
20 19 breq1d
 |-  ( ( d e. RR+ /\ f = d ) -> ( ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B <-> ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B ) )
21 15 20 imbi12d
 |-  ( ( d e. RR+ /\ f = d ) -> ( ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) <-> ( d <_ d -> ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B ) ) )
22 13 21 rspcdv
 |-  ( d e. RR+ -> ( A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) -> ( d <_ d -> ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B ) ) )
23 8 9 12 22 syl3c
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) -> ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B )
24 5 ad2antrr
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> F e. ( Poly ` RR ) )
25 simpr
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> d e. RR+ )
26 25 rpred
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> d e. RR )
27 24 26 plyrecld
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( F ` d ) e. RR )
28 dgrcl
 |-  ( F e. ( Poly ` RR ) -> ( deg ` F ) e. NN0 )
29 5 28 syl
 |-  ( ph -> ( deg ` F ) e. NN0 )
30 1 29 eqeltrid
 |-  ( ph -> D e. NN0 )
31 30 ad2antrr
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> D e. NN0 )
32 26 31 reexpcld
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( d ^ D ) e. RR )
33 25 rpcnd
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> d e. CC )
34 25 rpne0d
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> d =/= 0 )
35 30 nn0zd
 |-  ( ph -> D e. ZZ )
36 35 ad2antrr
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> D e. ZZ )
37 33 34 36 expne0d
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( d ^ D ) =/= 0 )
38 27 32 37 redivcld
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( ( F ` d ) / ( d ^ D ) ) e. RR )
39 0re
 |-  0 e. RR
40 2 coef2
 |-  ( ( F e. ( Poly ` RR ) /\ 0 e. RR ) -> C : NN0 --> RR )
41 39 40 mpan2
 |-  ( F e. ( Poly ` RR ) -> C : NN0 --> RR )
42 41 ffvelrnda
 |-  ( ( F e. ( Poly ` RR ) /\ D e. NN0 ) -> ( C ` D ) e. RR )
43 3 42 eqeltrid
 |-  ( ( F e. ( Poly ` RR ) /\ D e. NN0 ) -> B e. RR )
44 5 30 43 syl2anc
 |-  ( ph -> B e. RR )
45 44 ad2antrr
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> B e. RR )
46 45 renegcld
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> -u B e. RR )
47 38 45 46 absdifltd
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B <-> ( ( B - -u B ) < ( ( F ` d ) / ( d ^ D ) ) /\ ( ( F ` d ) / ( d ^ D ) ) < ( B + -u B ) ) ) )
48 47 simplbda
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B ) -> ( ( F ` d ) / ( d ^ D ) ) < ( B + -u B ) )
49 44 recnd
 |-  ( ph -> B e. CC )
50 49 ad2antrr
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> B e. CC )
51 50 negidd
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( B + -u B ) = 0 )
52 51 adantr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B ) -> ( B + -u B ) = 0 )
53 48 52 breqtrd
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B ) -> ( ( F ` d ) / ( d ^ D ) ) < 0 )
54 25 36 rpexpcld
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( d ^ D ) e. RR+ )
55 27 54 ge0divd
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( 0 <_ ( F ` d ) <-> 0 <_ ( ( F ` d ) / ( d ^ D ) ) ) )
56 55 notbid
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( -. 0 <_ ( F ` d ) <-> -. 0 <_ ( ( F ` d ) / ( d ^ D ) ) ) )
57 0red
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> 0 e. RR )
58 27 57 ltnled
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( ( F ` d ) < 0 <-> -. 0 <_ ( F ` d ) ) )
59 38 57 ltnled
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( ( ( F ` d ) / ( d ^ D ) ) < 0 <-> -. 0 <_ ( ( F ` d ) / ( d ^ D ) ) ) )
60 56 58 59 3bitr4d
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) -> ( ( F ` d ) < 0 <-> ( ( F ` d ) / ( d ^ D ) ) < 0 ) )
61 60 adantr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B ) -> ( ( F ` d ) < 0 <-> ( ( F ` d ) / ( d ^ D ) ) < 0 ) )
62 53 61 mpbird
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < -u B ) -> ( F ` d ) < 0 )
63 23 62 syldan
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) -> ( F ` d ) < 0 )
64 0red
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> 0 e. RR )
65 simplr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> d e. RR+ )
66 65 rpred
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> d e. RR )
67 65 rpgt0d
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> 0 < d )
68 iccssre
 |-  ( ( 0 e. RR /\ d e. RR ) -> ( 0 [,] d ) C_ RR )
69 39 66 68 sylancr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> ( 0 [,] d ) C_ RR )
70 ax-resscn
 |-  RR C_ CC
71 69 70 sstrdi
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> ( 0 [,] d ) C_ CC )
72 plycn
 |-  ( F e. ( Poly ` RR ) -> F e. ( CC -cn-> CC ) )
73 5 72 syl
 |-  ( ph -> F e. ( CC -cn-> CC ) )
74 73 ad3antrrr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> F e. ( CC -cn-> CC ) )
75 5 ad4antr
 |-  ( ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) /\ x e. ( 0 [,] d ) ) -> F e. ( Poly ` RR ) )
76 69 sselda
 |-  ( ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) /\ x e. ( 0 [,] d ) ) -> x e. RR )
77 75 76 plyrecld
 |-  ( ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) /\ x e. ( 0 [,] d ) ) -> ( F ` x ) e. RR )
78 simpr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> ( F ` d ) < 0 )
79 simplll
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> ph )
80 79 44 syl
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> B e. RR )
81 simpr
 |-  ( ( ph /\ -u B e. RR+ ) -> -u B e. RR+ )
82 81 ad2antrr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> -u B e. RR+ )
83 negelrp
 |-  ( B e. RR -> ( -u B e. RR+ <-> B < 0 ) )
84 83 biimpa
 |-  ( ( B e. RR /\ -u B e. RR+ ) -> B < 0 )
85 80 82 84 syl2anc
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> B < 0 )
86 5 39 40 sylancl
 |-  ( ph -> C : NN0 --> RR )
87 0nn0
 |-  0 e. NN0
88 87 a1i
 |-  ( ph -> 0 e. NN0 )
89 86 88 ffvelrnd
 |-  ( ph -> ( C ` 0 ) e. RR )
90 4 89 eqeltrid
 |-  ( ph -> A e. RR )
91 90 44 7 mul2lt0rlt0
 |-  ( ( ph /\ B < 0 ) -> 0 < A )
92 91 4 breqtrdi
 |-  ( ( ph /\ B < 0 ) -> 0 < ( C ` 0 ) )
93 79 85 92 syl2anc
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> 0 < ( C ` 0 ) )
94 2 coefv0
 |-  ( F e. ( Poly ` RR ) -> ( F ` 0 ) = ( C ` 0 ) )
95 5 94 syl
 |-  ( ph -> ( F ` 0 ) = ( C ` 0 ) )
96 95 ad3antrrr
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> ( F ` 0 ) = ( C ` 0 ) )
97 93 96 breqtrrd
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> 0 < ( F ` 0 ) )
98 78 97 jca
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> ( ( F ` d ) < 0 /\ 0 < ( F ` 0 ) ) )
99 64 66 64 67 71 74 77 98 ivth2
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> E. z e. ( 0 (,) d ) ( F ` z ) = 0 )
100 0le0
 |-  0 <_ 0
101 pnfge
 |-  ( d e. RR* -> d <_ +oo )
102 10 101 syl
 |-  ( d e. RR+ -> d <_ +oo )
103 0xr
 |-  0 e. RR*
104 pnfxr
 |-  +oo e. RR*
105 ioossioo
 |-  ( ( ( 0 e. RR* /\ +oo e. RR* ) /\ ( 0 <_ 0 /\ d <_ +oo ) ) -> ( 0 (,) d ) C_ ( 0 (,) +oo ) )
106 103 104 105 mpanl12
 |-  ( ( 0 <_ 0 /\ d <_ +oo ) -> ( 0 (,) d ) C_ ( 0 (,) +oo ) )
107 100 102 106 sylancr
 |-  ( d e. RR+ -> ( 0 (,) d ) C_ ( 0 (,) +oo ) )
108 ioorp
 |-  ( 0 (,) +oo ) = RR+
109 107 108 sseqtrdi
 |-  ( d e. RR+ -> ( 0 (,) d ) C_ RR+ )
110 ssrexv
 |-  ( ( 0 (,) d ) C_ RR+ -> ( E. z e. ( 0 (,) d ) ( F ` z ) = 0 -> E. z e. RR+ ( F ` z ) = 0 ) )
111 65 109 110 3syl
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> ( E. z e. ( 0 (,) d ) ( F ` z ) = 0 -> E. z e. RR+ ( F ` z ) = 0 ) )
112 99 111 mpd
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ ( F ` d ) < 0 ) -> E. z e. RR+ ( F ` z ) = 0 )
113 63 112 syldan
 |-  ( ( ( ( ph /\ -u B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) -> E. z e. RR+ ( F ` z ) = 0 )
114 plyf
 |-  ( F e. ( Poly ` RR ) -> F : CC --> CC )
115 5 114 syl
 |-  ( ph -> F : CC --> CC )
116 115 ffnd
 |-  ( ph -> F Fn CC )
117 ovex
 |-  ( x ^ D ) e. _V
118 117 rgenw
 |-  A. x e. RR+ ( x ^ D ) e. _V
119 eqid
 |-  ( x e. RR+ |-> ( x ^ D ) ) = ( x e. RR+ |-> ( x ^ D ) )
120 119 fnmpt
 |-  ( A. x e. RR+ ( x ^ D ) e. _V -> ( x e. RR+ |-> ( x ^ D ) ) Fn RR+ )
121 118 120 mp1i
 |-  ( ph -> ( x e. RR+ |-> ( x ^ D ) ) Fn RR+ )
122 cnex
 |-  CC e. _V
123 122 a1i
 |-  ( ph -> CC e. _V )
124 rpssre
 |-  RR+ C_ RR
125 124 70 sstri
 |-  RR+ C_ CC
126 122 125 ssexi
 |-  RR+ e. _V
127 126 a1i
 |-  ( ph -> RR+ e. _V )
128 sseqin2
 |-  ( RR+ C_ CC <-> ( CC i^i RR+ ) = RR+ )
129 125 128 mpbi
 |-  ( CC i^i RR+ ) = RR+
130 eqidd
 |-  ( ( ph /\ f e. CC ) -> ( F ` f ) = ( F ` f ) )
131 eqidd
 |-  ( ( ph /\ f e. RR+ ) -> ( x e. RR+ |-> ( x ^ D ) ) = ( x e. RR+ |-> ( x ^ D ) ) )
132 simpr
 |-  ( ( ( ph /\ f e. RR+ ) /\ x = f ) -> x = f )
133 132 oveq1d
 |-  ( ( ( ph /\ f e. RR+ ) /\ x = f ) -> ( x ^ D ) = ( f ^ D ) )
134 simpr
 |-  ( ( ph /\ f e. RR+ ) -> f e. RR+ )
135 ovexd
 |-  ( ( ph /\ f e. RR+ ) -> ( f ^ D ) e. _V )
136 131 133 134 135 fvmptd
 |-  ( ( ph /\ f e. RR+ ) -> ( ( x e. RR+ |-> ( x ^ D ) ) ` f ) = ( f ^ D ) )
137 116 121 123 127 129 130 136 offval
 |-  ( ph -> ( F oF / ( x e. RR+ |-> ( x ^ D ) ) ) = ( f e. RR+ |-> ( ( F ` f ) / ( f ^ D ) ) ) )
138 oveq1
 |-  ( x = f -> ( x ^ D ) = ( f ^ D ) )
139 138 cbvmptv
 |-  ( x e. RR+ |-> ( x ^ D ) ) = ( f e. RR+ |-> ( f ^ D ) )
140 1 2 3 139 signsplypnf
 |-  ( F e. ( Poly ` RR ) -> ( F oF / ( x e. RR+ |-> ( x ^ D ) ) ) ~~>r B )
141 5 140 syl
 |-  ( ph -> ( F oF / ( x e. RR+ |-> ( x ^ D ) ) ) ~~>r B )
142 137 141 eqbrtrrd
 |-  ( ph -> ( f e. RR+ |-> ( ( F ` f ) / ( f ^ D ) ) ) ~~>r B )
143 115 adantr
 |-  ( ( ph /\ f e. RR+ ) -> F : CC --> CC )
144 134 rpcnd
 |-  ( ( ph /\ f e. RR+ ) -> f e. CC )
145 143 144 ffvelrnd
 |-  ( ( ph /\ f e. RR+ ) -> ( F ` f ) e. CC )
146 30 adantr
 |-  ( ( ph /\ f e. RR+ ) -> D e. NN0 )
147 144 146 expcld
 |-  ( ( ph /\ f e. RR+ ) -> ( f ^ D ) e. CC )
148 134 rpne0d
 |-  ( ( ph /\ f e. RR+ ) -> f =/= 0 )
149 35 adantr
 |-  ( ( ph /\ f e. RR+ ) -> D e. ZZ )
150 144 148 149 expne0d
 |-  ( ( ph /\ f e. RR+ ) -> ( f ^ D ) =/= 0 )
151 145 147 150 divcld
 |-  ( ( ph /\ f e. RR+ ) -> ( ( F ` f ) / ( f ^ D ) ) e. CC )
152 151 ralrimiva
 |-  ( ph -> A. f e. RR+ ( ( F ` f ) / ( f ^ D ) ) e. CC )
153 124 a1i
 |-  ( ph -> RR+ C_ RR )
154 1red
 |-  ( ph -> 1 e. RR )
155 152 153 49 154 rlim3
 |-  ( ph -> ( ( f e. RR+ |-> ( ( F ` f ) / ( f ^ D ) ) ) ~~>r B <-> A. e e. RR+ E. d e. ( 1 [,) +oo ) A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) ) )
156 142 155 mpbid
 |-  ( ph -> A. e e. RR+ E. d e. ( 1 [,) +oo ) A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) )
157 0lt1
 |-  0 < 1
158 pnfge
 |-  ( +oo e. RR* -> +oo <_ +oo )
159 104 158 ax-mp
 |-  +oo <_ +oo
160 icossioo
 |-  ( ( ( 0 e. RR* /\ +oo e. RR* ) /\ ( 0 < 1 /\ +oo <_ +oo ) ) -> ( 1 [,) +oo ) C_ ( 0 (,) +oo ) )
161 103 104 157 159 160 mp4an
 |-  ( 1 [,) +oo ) C_ ( 0 (,) +oo )
162 161 108 sseqtri
 |-  ( 1 [,) +oo ) C_ RR+
163 ssrexv
 |-  ( ( 1 [,) +oo ) C_ RR+ -> ( E. d e. ( 1 [,) +oo ) A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) -> E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) ) )
164 162 163 ax-mp
 |-  ( E. d e. ( 1 [,) +oo ) A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) -> E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) )
165 164 ralimi
 |-  ( A. e e. RR+ E. d e. ( 1 [,) +oo ) A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) -> A. e e. RR+ E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) )
166 156 165 syl
 |-  ( ph -> A. e e. RR+ E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) )
167 166 adantr
 |-  ( ( ph /\ -u B e. RR+ ) -> A. e e. RR+ E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) )
168 simpr
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ e = -u B ) -> e = -u B )
169 168 breq2d
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ e = -u B ) -> ( ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e <-> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) )
170 169 imbi2d
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ e = -u B ) -> ( ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) <-> ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) )
171 170 rexralbidv
 |-  ( ( ( ph /\ -u B e. RR+ ) /\ e = -u B ) -> ( E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) <-> E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) )
172 81 171 rspcdv
 |-  ( ( ph /\ -u B e. RR+ ) -> ( A. e e. RR+ E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) -> E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) ) )
173 167 172 mpd
 |-  ( ( ph /\ -u B e. RR+ ) -> E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < -u B ) )
174 113 173 r19.29a
 |-  ( ( ph /\ -u B e. RR+ ) -> E. z e. RR+ ( F ` z ) = 0 )
175 simplr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) -> d e. RR+ )
176 simpr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) -> A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) )
177 11 ad2antlr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) -> d <_ d )
178 19 breq1d
 |-  ( ( d e. RR+ /\ f = d ) -> ( ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B <-> ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B ) )
179 15 178 imbi12d
 |-  ( ( d e. RR+ /\ f = d ) -> ( ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) <-> ( d <_ d -> ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B ) ) )
180 13 179 rspcdv
 |-  ( d e. RR+ -> ( A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) -> ( d <_ d -> ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B ) ) )
181 175 176 177 180 syl3c
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) -> ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B )
182 49 ad2antrr
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> B e. CC )
183 182 subidd
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> ( B - B ) = 0 )
184 183 adantr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B ) -> ( B - B ) = 0 )
185 5 ad2antrr
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> F e. ( Poly ` RR ) )
186 124 a1i
 |-  ( ( ph /\ B e. RR+ ) -> RR+ C_ RR )
187 186 sselda
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> d e. RR )
188 185 187 plyrecld
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> ( F ` d ) e. RR )
189 30 ad2antrr
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> D e. NN0 )
190 187 189 reexpcld
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> ( d ^ D ) e. RR )
191 187 recnd
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> d e. CC )
192 simpr
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> d e. RR+ )
193 192 rpne0d
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> d =/= 0 )
194 35 ad2antrr
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> D e. ZZ )
195 191 193 194 expne0d
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> ( d ^ D ) =/= 0 )
196 188 190 195 redivcld
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> ( ( F ` d ) / ( d ^ D ) ) e. RR )
197 44 ad2antrr
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> B e. RR )
198 196 197 197 absdifltd
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> ( ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B <-> ( ( B - B ) < ( ( F ` d ) / ( d ^ D ) ) /\ ( ( F ` d ) / ( d ^ D ) ) < ( B + B ) ) ) )
199 198 simprbda
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B ) -> ( B - B ) < ( ( F ` d ) / ( d ^ D ) ) )
200 184 199 eqbrtrrd
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B ) -> 0 < ( ( F ` d ) / ( d ^ D ) ) )
201 192 194 rpexpcld
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> ( d ^ D ) e. RR+ )
202 188 201 gt0divd
 |-  ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) -> ( 0 < ( F ` d ) <-> 0 < ( ( F ` d ) / ( d ^ D ) ) ) )
203 202 adantr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B ) -> ( 0 < ( F ` d ) <-> 0 < ( ( F ` d ) / ( d ^ D ) ) ) )
204 200 203 mpbird
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ ( abs ` ( ( ( F ` d ) / ( d ^ D ) ) - B ) ) < B ) -> 0 < ( F ` d ) )
205 181 204 syldan
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) -> 0 < ( F ` d ) )
206 0red
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> 0 e. RR )
207 simplr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> d e. RR+ )
208 207 rpred
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> d e. RR )
209 207 rpgt0d
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> 0 < d )
210 39 208 68 sylancr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> ( 0 [,] d ) C_ RR )
211 210 70 sstrdi
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> ( 0 [,] d ) C_ CC )
212 73 ad3antrrr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> F e. ( CC -cn-> CC ) )
213 5 ad4antr
 |-  ( ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) /\ x e. ( 0 [,] d ) ) -> F e. ( Poly ` RR ) )
214 210 sselda
 |-  ( ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) /\ x e. ( 0 [,] d ) ) -> x e. RR )
215 213 214 plyrecld
 |-  ( ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) /\ x e. ( 0 [,] d ) ) -> ( F ` x ) e. RR )
216 95 ad3antrrr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> ( F ` 0 ) = ( C ` 0 ) )
217 simplll
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> ph )
218 simpr1
 |-  ( ( ph /\ ( B e. RR+ /\ d e. RR+ /\ 0 < ( F ` d ) ) ) -> B e. RR+ )
219 218 rpgt0d
 |-  ( ( ph /\ ( B e. RR+ /\ d e. RR+ /\ 0 < ( F ` d ) ) ) -> 0 < B )
220 219 3anassrs
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> 0 < B )
221 90 44 7 mul2lt0rgt0
 |-  ( ( ph /\ 0 < B ) -> A < 0 )
222 217 220 221 syl2anc
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> A < 0 )
223 4 222 eqbrtrrid
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> ( C ` 0 ) < 0 )
224 216 223 eqbrtrd
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> ( F ` 0 ) < 0 )
225 simpr
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> 0 < ( F ` d ) )
226 224 225 jca
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> ( ( F ` 0 ) < 0 /\ 0 < ( F ` d ) ) )
227 206 208 206 209 211 212 215 226 ivth
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> E. z e. ( 0 (,) d ) ( F ` z ) = 0 )
228 207 109 110 3syl
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> ( E. z e. ( 0 (,) d ) ( F ` z ) = 0 -> E. z e. RR+ ( F ` z ) = 0 ) )
229 227 228 mpd
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ 0 < ( F ` d ) ) -> E. z e. RR+ ( F ` z ) = 0 )
230 205 229 syldan
 |-  ( ( ( ( ph /\ B e. RR+ ) /\ d e. RR+ ) /\ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) -> E. z e. RR+ ( F ` z ) = 0 )
231 166 adantr
 |-  ( ( ph /\ B e. RR+ ) -> A. e e. RR+ E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) )
232 simpr
 |-  ( ( ph /\ B e. RR+ ) -> B e. RR+ )
233 simpr
 |-  ( ( ( ph /\ B e. RR+ ) /\ e = B ) -> e = B )
234 233 breq2d
 |-  ( ( ( ph /\ B e. RR+ ) /\ e = B ) -> ( ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e <-> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) )
235 234 imbi2d
 |-  ( ( ( ph /\ B e. RR+ ) /\ e = B ) -> ( ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) <-> ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) )
236 235 rexralbidv
 |-  ( ( ( ph /\ B e. RR+ ) /\ e = B ) -> ( E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) <-> E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) )
237 232 236 rspcdv
 |-  ( ( ph /\ B e. RR+ ) -> ( A. e e. RR+ E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < e ) -> E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) ) )
238 231 237 mpd
 |-  ( ( ph /\ B e. RR+ ) -> E. d e. RR+ A. f e. RR+ ( d <_ f -> ( abs ` ( ( ( F ` f ) / ( f ^ D ) ) - B ) ) < B ) )
239 230 238 r19.29a
 |-  ( ( ph /\ B e. RR+ ) -> E. z e. RR+ ( F ` z ) = 0 )
240 1 2 dgreq0
 |-  ( F e. ( Poly ` RR ) -> ( F = 0p <-> ( C ` D ) = 0 ) )
241 5 240 syl
 |-  ( ph -> ( F = 0p <-> ( C ` D ) = 0 ) )
242 241 necon3bid
 |-  ( ph -> ( F =/= 0p <-> ( C ` D ) =/= 0 ) )
243 6 242 mpbid
 |-  ( ph -> ( C ` D ) =/= 0 )
244 3 neeq1i
 |-  ( B =/= 0 <-> ( C ` D ) =/= 0 )
245 243 244 sylibr
 |-  ( ph -> B =/= 0 )
246 rpneg
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( B e. RR+ <-> -. -u B e. RR+ ) )
247 246 biimprd
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( -. -u B e. RR+ -> B e. RR+ ) )
248 247 orrd
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( -u B e. RR+ \/ B e. RR+ ) )
249 44 245 248 syl2anc
 |-  ( ph -> ( -u B e. RR+ \/ B e. RR+ ) )
250 174 239 249 mpjaodan
 |-  ( ph -> E. z e. RR+ ( F ` z ) = 0 )