Metamath Proof Explorer

Theorem signsplypnf

Description: The quotient of a polynomial F by a monic monomial of same degree G converges to the highest coefficient of F . (Contributed by Thierry Arnoux, 18-Sep-2018)

Ref Expression
Hypotheses signsply0.d 
|- D = ( deg ` F )
signsply0.c 
|- C = ( coeff ` F )
signsply0.b 
|- B = ( C ` D )
signsplypnf.g 
|- G = ( x e. RR+ |-> ( x ^ D ) )
Assertion signsplypnf 
|- ( F e. ( Poly ` RR ) -> ( F oF / G ) ~~>r B )

Proof

Step Hyp Ref Expression
1 signsply0.d 
 |-  D = ( deg ` F )
2 signsply0.c 
 |-  C = ( coeff ` F )
3 signsply0.b 
 |-  B = ( C ` D )
4 signsplypnf.g 
 |-  G = ( x e. RR+ |-> ( x ^ D ) )
5 plyf 
 |-  ( F e. ( Poly ` RR ) -> F : CC --> CC )
6 5 ffnd 
 |-  ( F e. ( Poly ` RR ) -> F Fn CC )
7 ovex 
 |-  ( x ^ D ) e. _V
8 7 rgenw 
 |-  A. x e. RR+ ( x ^ D ) e. _V
9 4 fnmpt 
 |-  ( A. x e. RR+ ( x ^ D ) e. _V -> G Fn RR+ )
10 8 9 mp1i 
 |-  ( F e. ( Poly ` RR ) -> G Fn RR+ )
11 cnex 
 |-  CC e. _V
12 11 a1i 
 |-  ( F e. ( Poly ` RR ) -> CC e. _V )
13 reex 
 |-  RR e. _V
14 rpssre 
 |-  RR+ C_ RR
15 13 14 ssexi 
 |-  RR+ e. _V
16 15 a1i 
 |-  ( F e. ( Poly ` RR ) -> RR+ e. _V )
17 ax-resscn 
 |-  RR C_ CC
18 14 17 sstri 
 |-  RR+ C_ CC
19 sseqin2 
 |-  ( RR+ C_ CC <-> ( CC i^i RR+ ) = RR+ )
20 18 19 mpbi 
 |-  ( CC i^i RR+ ) = RR+
21 2 1 coeid2 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. CC ) -> ( F ` x ) = sum_ k e. ( 0 ... D ) ( ( C ` k ) x. ( x ^ k ) ) )
22 4 fvmpt2 
 |-  ( ( x e. RR+ /\ ( x ^ D ) e. _V ) -> ( G ` x ) = ( x ^ D ) )
23 7 22 mpan2 
 |-  ( x e. RR+ -> ( G ` x ) = ( x ^ D ) )
24 23 adantl 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( G ` x ) = ( x ^ D ) )
25 6 10 12 16 20 21 24 offval 
 |-  ( F e. ( Poly ` RR ) -> ( F oF / G ) = ( x e. RR+ |-> ( sum_ k e. ( 0 ... D ) ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) )
26 fzfid 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( 0 ... D ) e. Fin )
27 18 a1i 
 |-  ( F e. ( Poly ` RR ) -> RR+ C_ CC )
28 27 sselda 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> x e. CC )
29 dgrcl 
 |-  ( F e. ( Poly ` RR ) -> ( deg ` F ) e. NN0 )
30 1 29 eqeltrid 
 |-  ( F e. ( Poly ` RR ) -> D e. NN0 )
31 30 adantr 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> D e. NN0 )
32 28 31 expcld 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( x ^ D ) e. CC )
33 2 coef3 
 |-  ( F e. ( Poly ` RR ) -> C : NN0 --> CC )
34 33 ad2antrr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> C : NN0 --> CC )
35 elfznn0 
 |-  ( k e. ( 0 ... D ) -> k e. NN0 )
36 35 adantl 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> k e. NN0 )
37 34 36 ffvelrnd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> ( C ` k ) e. CC )
38 28 adantr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> x e. CC )
39 38 36 expcld 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> ( x ^ k ) e. CC )
40 37 39 mulcld 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> ( ( C ` k ) x. ( x ^ k ) ) e. CC )
41 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
42 41 adantl 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> x =/= 0 )
43 30 nn0zd 
 |-  ( F e. ( Poly ` RR ) -> D e. ZZ )
44 43 adantr 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> D e. ZZ )
45 28 42 44 expne0d 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( x ^ D ) =/= 0 )
46 26 32 40 45 fsumdivc 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( sum_ k e. ( 0 ... D ) ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) = sum_ k e. ( 0 ... D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) )
47 fzosn 
 |-  ( D e. ZZ -> ( D ..^ ( D + 1 ) ) = { D } )
48 47 ineq2d 
 |-  ( D e. ZZ -> ( ( 0 ..^ D ) i^i ( D ..^ ( D + 1 ) ) ) = ( ( 0 ..^ D ) i^i { D } ) )
49 fzodisj 
 |-  ( ( 0 ..^ D ) i^i ( D ..^ ( D + 1 ) ) ) = (/)
50 48 49 eqtr3di 
 |-  ( D e. ZZ -> ( ( 0 ..^ D ) i^i { D } ) = (/) )
51 44 50 syl 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( ( 0 ..^ D ) i^i { D } ) = (/) )
52 fzval3 
 |-  ( D e. ZZ -> ( 0 ... D ) = ( 0 ..^ ( D + 1 ) ) )
53 43 52 syl 
 |-  ( F e. ( Poly ` RR ) -> ( 0 ... D ) = ( 0 ..^ ( D + 1 ) ) )
54 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
55 30 54 eleqtrdi 
 |-  ( F e. ( Poly ` RR ) -> D e. ( ZZ>= ` 0 ) )
56 fzosplitsn 
 |-  ( D e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( D + 1 ) ) = ( ( 0 ..^ D ) u. { D } ) )
57 55 56 syl 
 |-  ( F e. ( Poly ` RR ) -> ( 0 ..^ ( D + 1 ) ) = ( ( 0 ..^ D ) u. { D } ) )
58 53 57 eqtrd 
 |-  ( F e. ( Poly ` RR ) -> ( 0 ... D ) = ( ( 0 ..^ D ) u. { D } ) )
59 58 adantr 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( 0 ... D ) = ( ( 0 ..^ D ) u. { D } ) )
60 32 adantr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> ( x ^ D ) e. CC )
61 42 adantr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> x =/= 0 )
62 44 adantr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> D e. ZZ )
63 38 61 62 expne0d 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> ( x ^ D ) =/= 0 )
64 40 60 63 divcld 
 |-  ( ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) /\ k e. ( 0 ... D ) ) -> ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) e. CC )
65 51 59 26 64 fsumsplit 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> sum_ k e. ( 0 ... D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) = ( sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) + sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) )
66 46 65 eqtrd 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( sum_ k e. ( 0 ... D ) ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) = ( sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) + sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) )
67 66 mpteq2dva 
 |-  ( F e. ( Poly ` RR ) -> ( x e. RR+ |-> ( sum_ k e. ( 0 ... D ) ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) = ( x e. RR+ |-> ( sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) + sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) ) )
68 25 67 eqtrd 
 |-  ( F e. ( Poly ` RR ) -> ( F oF / G ) = ( x e. RR+ |-> ( sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) + sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) ) )
69 sumex 
 |-  sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) e. _V
70 69 a1i 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) e. _V )
71 sumex 
 |-  sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) e. _V
72 71 a1i 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) e. _V )
73 14 a1i 
 |-  ( F e. ( Poly ` RR ) -> RR+ C_ RR )
74 fzofi 
 |-  ( 0 ..^ D ) e. Fin
75 74 a1i 
 |-  ( F e. ( Poly ` RR ) -> ( 0 ..^ D ) e. Fin )
76 ovexd 
 |-  ( ( F e. ( Poly ` RR ) /\ ( x e. RR+ /\ k e. ( 0 ..^ D ) ) ) -> ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) e. _V )
77 33 ad2antrr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> C : NN0 --> CC )
78 elfzonn0 
 |-  ( k e. ( 0 ..^ D ) -> k e. NN0 )
79 78 ad2antlr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> k e. NN0 )
80 77 79 ffvelrnd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( C ` k ) e. CC )
81 28 adantlr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> x e. CC )
82 81 79 expcld 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( x ^ k ) e. CC )
83 32 adantlr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( x ^ D ) e. CC )
84 41 adantl 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> x =/= 0 )
85 44 adantlr 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> D e. ZZ )
86 81 84 85 expne0d 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( x ^ D ) =/= 0 )
87 80 82 83 86 divassd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) = ( ( C ` k ) x. ( ( x ^ k ) / ( x ^ D ) ) ) )
88 87 mpteq2dva 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( x e. RR+ |-> ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) = ( x e. RR+ |-> ( ( C ` k ) x. ( ( x ^ k ) / ( x ^ D ) ) ) ) )
89 fvexd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( C ` k ) e. _V )
90 ovexd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( ( x ^ k ) / ( x ^ D ) ) e. _V )
91 33 adantr 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> C : NN0 --> CC )
92 78 adantl 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> k e. NN0 )
93 91 92 ffvelrnd 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( C ` k ) e. CC )
94 rlimconst 
 |-  ( ( RR+ C_ RR /\ ( C ` k ) e. CC ) -> ( x e. RR+ |-> ( C ` k ) ) ~~>r ( C ` k ) )
95 14 93 94 sylancr 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( x e. RR+ |-> ( C ` k ) ) ~~>r ( C ` k ) )
96 79 nn0zd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> k e. ZZ )
97 85 96 zsubcld 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( D - k ) e. ZZ )
98 81 84 97 cxpexpzd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( x ^c ( D - k ) ) = ( x ^ ( D - k ) ) )
99 98 oveq2d 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( 1 / ( x ^c ( D - k ) ) ) = ( 1 / ( x ^ ( D - k ) ) ) )
100 81 84 97 expnegd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( x ^ -u ( D - k ) ) = ( 1 / ( x ^ ( D - k ) ) ) )
101 85 zcnd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> D e. CC )
102 79 nn0cnd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> k e. CC )
103 101 102 negsubdi2d 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> -u ( D - k ) = ( k - D ) )
104 103 oveq2d 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( x ^ -u ( D - k ) ) = ( x ^ ( k - D ) ) )
105 99 100 104 3eqtr2d 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( 1 / ( x ^c ( D - k ) ) ) = ( x ^ ( k - D ) ) )
106 81 84 85 96 expsubd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( x ^ ( k - D ) ) = ( ( x ^ k ) / ( x ^ D ) ) )
107 105 106 eqtrd 
 |-  ( ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) /\ x e. RR+ ) -> ( 1 / ( x ^c ( D - k ) ) ) = ( ( x ^ k ) / ( x ^ D ) ) )
108 107 mpteq2dva 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( x e. RR+ |-> ( 1 / ( x ^c ( D - k ) ) ) ) = ( x e. RR+ |-> ( ( x ^ k ) / ( x ^ D ) ) ) )
109 92 nn0red 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> k e. RR )
110 30 adantr 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> D e. NN0 )
111 110 nn0red 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> D e. RR )
112 elfzolt2 
 |-  ( k e. ( 0 ..^ D ) -> k < D )
113 112 adantl 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> k < D )
114 difrp 
 |-  ( ( k e. RR /\ D e. RR ) -> ( k < D <-> ( D - k ) e. RR+ ) )
115 114 biimpa 
 |-  ( ( ( k e. RR /\ D e. RR ) /\ k < D ) -> ( D - k ) e. RR+ )
116 109 111 113 115 syl21anc 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( D - k ) e. RR+ )
117 cxplim 
 |-  ( ( D - k ) e. RR+ -> ( x e. RR+ |-> ( 1 / ( x ^c ( D - k ) ) ) ) ~~>r 0 )
118 116 117 syl 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( x e. RR+ |-> ( 1 / ( x ^c ( D - k ) ) ) ) ~~>r 0 )
119 108 118 eqbrtrrd 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( x e. RR+ |-> ( ( x ^ k ) / ( x ^ D ) ) ) ~~>r 0 )
120 89 90 95 119 rlimmul 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( x e. RR+ |-> ( ( C ` k ) x. ( ( x ^ k ) / ( x ^ D ) ) ) ) ~~>r ( ( C ` k ) x. 0 ) )
121 93 mul01d 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( ( C ` k ) x. 0 ) = 0 )
122 120 121 breqtrd 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( x e. RR+ |-> ( ( C ` k ) x. ( ( x ^ k ) / ( x ^ D ) ) ) ) ~~>r 0 )
123 88 122 eqbrtrd 
 |-  ( ( F e. ( Poly ` RR ) /\ k e. ( 0 ..^ D ) ) -> ( x e. RR+ |-> ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) ~~>r 0 )
124 73 75 76 123 fsumrlim 
 |-  ( F e. ( Poly ` RR ) -> ( x e. RR+ |-> sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) ~~>r sum_ k e. ( 0 ..^ D ) 0 )
125 75 olcd 
 |-  ( F e. ( Poly ` RR ) -> ( ( 0 ..^ D ) C_ ( ZZ>= ` 0 ) \/ ( 0 ..^ D ) e. Fin ) )
126 sumz 
 |-  ( ( ( 0 ..^ D ) C_ ( ZZ>= ` 0 ) \/ ( 0 ..^ D ) e. Fin ) -> sum_ k e. ( 0 ..^ D ) 0 = 0 )
127 125 126 syl 
 |-  ( F e. ( Poly ` RR ) -> sum_ k e. ( 0 ..^ D ) 0 = 0 )
128 124 127 breqtrd 
 |-  ( F e. ( Poly ` RR ) -> ( x e. RR+ |-> sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) ~~>r 0 )
129 33 30 ffvelrnd 
 |-  ( F e. ( Poly ` RR ) -> ( C ` D ) e. CC )
130 129 adantr 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( C ` D ) e. CC )
131 130 32 mulcld 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( ( C ` D ) x. ( x ^ D ) ) e. CC )
132 131 32 45 divcld 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( ( ( C ` D ) x. ( x ^ D ) ) / ( x ^ D ) ) e. CC )
133 fveq2 
 |-  ( k = D -> ( C ` k ) = ( C ` D ) )
134 oveq2 
 |-  ( k = D -> ( x ^ k ) = ( x ^ D ) )
135 133 134 oveq12d 
 |-  ( k = D -> ( ( C ` k ) x. ( x ^ k ) ) = ( ( C ` D ) x. ( x ^ D ) ) )
136 135 oveq1d 
 |-  ( k = D -> ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) = ( ( ( C ` D ) x. ( x ^ D ) ) / ( x ^ D ) ) )
137 136 sumsn 
 |-  ( ( D e. NN0 /\ ( ( ( C ` D ) x. ( x ^ D ) ) / ( x ^ D ) ) e. CC ) -> sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) = ( ( ( C ` D ) x. ( x ^ D ) ) / ( x ^ D ) ) )
138 31 132 137 syl2anc 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) = ( ( ( C ` D ) x. ( x ^ D ) ) / ( x ^ D ) ) )
139 130 32 45 divcan4d 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> ( ( ( C ` D ) x. ( x ^ D ) ) / ( x ^ D ) ) = ( C ` D ) )
140 138 139 eqtrd 
 |-  ( ( F e. ( Poly ` RR ) /\ x e. RR+ ) -> sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) = ( C ` D ) )
141 140 mpteq2dva 
 |-  ( F e. ( Poly ` RR ) -> ( x e. RR+ |-> sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) = ( x e. RR+ |-> ( C ` D ) ) )
142 rlimconst 
 |-  ( ( RR+ C_ RR /\ ( C ` D ) e. CC ) -> ( x e. RR+ |-> ( C ` D ) ) ~~>r ( C ` D ) )
143 14 129 142 sylancr 
 |-  ( F e. ( Poly ` RR ) -> ( x e. RR+ |-> ( C ` D ) ) ~~>r ( C ` D ) )
144 141 143 eqbrtrd 
 |-  ( F e. ( Poly ` RR ) -> ( x e. RR+ |-> sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) ~~>r ( C ` D ) )
145 70 72 128 144 rlimadd 
 |-  ( F e. ( Poly ` RR ) -> ( x e. RR+ |-> ( sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) + sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) ) ~~>r ( 0 + ( C ` D ) ) )
146 129 addid2d 
 |-  ( F e. ( Poly ` RR ) -> ( 0 + ( C ` D ) ) = ( C ` D ) )
147 146 3 eqtr4di 
 |-  ( F e. ( Poly ` RR ) -> ( 0 + ( C ` D ) ) = B )
148 145 147 breqtrd 
 |-  ( F e. ( Poly ` RR ) -> ( x e. RR+ |-> ( sum_ k e. ( 0 ..^ D ) ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) + sum_ k e. { D } ( ( ( C ` k ) x. ( x ^ k ) ) / ( x ^ D ) ) ) ) ~~>r B )
149 68 148 eqbrtrd 
 |-  ( F e. ( Poly ` RR ) -> ( F oF / G ) ~~>r B )