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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( ( 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 )