let g be Function of NAT,REAL; :: thesis: ( g = (polynom c) (#) f implies g is negligible )
assume A0: g = (polynom c) (#) f ; :: thesis: g is negligible
let s be non empty positive-yielding XFinSequence of REAL ; :: according to ASYMPT_3:def 4 :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(g . x).| < 1 / ((polynom s) . x)
consider d being non empty positive-yielding XFinSequence of REAL , N0 being Nat such that
P1: for x being Nat st N0 <= x holds
((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x by RNG0;
consider N1 being Nat such that
P2: for x being Nat st N1 <= x holds
|.(f . x).| < 1 / ((polynom d) . x) by defneg;
take N = N0 + N1; :: thesis: for x being Nat st N <= x holds
|.(g . x).| < 1 / ((polynom s) . x)
let x be Nat; :: thesis: ( N <= x implies |.(g . x).| < 1 / ((polynom s) . x) )
assume P3: N <= x ; :: thesis: |.(g . x).| < 1 / ((polynom s) . x)
P4: 0 < (polynom c) . x by NLM3;
Q4: 0 < (polynom d) . x by NLM3;
N1 <= N by NAT_1:12;
then N1 <= x by P3, XXREAL_0:2;
then P7: |.(f . x).| < 1 / ((polynom d) . x) by P2;
P6: |.(f . x).| * ((polynom c) . x) < (1 / ((polynom d) . x)) * ((polynom c) . x) by P7, P4, XREAL_1:97;
Q6: 0 < (polynom s) . x by NLM3;
N0 <= N by NAT_1:12;
then N0 <= x by P3, XXREAL_0:2;
then ((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x by P1;
then 1 / ((polynom d) . x) <= 1 / (((polynom c) . x) * ((polynom s) . x)) by P4, Q6, XREAL_1:118;
then P8: (1 / ((polynom d) . x)) * ((polynom c) . x) <= (1 / (((polynom c) . x) * ((polynom s) . x))) * ((polynom c) . x) by Q4, P4, XREAL_1:66;
P5: (1 / (((polynom c) . x) * ((polynom s) . x))) * ((polynom c) . x) = 1 / ((polynom s) . x) by P4, XCMPLX_1:92;
|.(f . x).| * ((polynom c) . x) = |.(f . x).| * |.((polynom c) . x).| by P4, ABSVALUE:def 1
.= |.(((polynom c) . x) * (f . x)).| by COMPLEX1:65
.= |.(((polynom c) (#) f) . x).| by VALUED_1:5 ;
hence |.(g . x).| < 1 / ((polynom s) . x) by A0, P5, XXREAL_0:2, P6, P8; :: thesis: verum