let x, r be Real; ( x > 0 & r > 0 implies Maclaurin (exp_R,].(- r),r.[,x) is positive-yielding )
assume A0:
( x > 0 & r > 0 )
; Maclaurin (exp_R,].(- r),r.[,x) is positive-yielding
set f = Maclaurin (exp_R,].(- r),r.[,x);
for r being Real st r in rng (Maclaurin (exp_R,].(- r),r.[,x)) holds
0 < r
proof
let r be
Real;
( r in rng (Maclaurin (exp_R,].(- r),r.[,x)) implies 0 < r )
assume
r in rng (Maclaurin (exp_R,].(- r),r.[,x))
;
0 < r
then consider xx being
object such that A1:
(
xx in dom (Maclaurin (exp_R,].(- r),r.[,x)) &
r = (Maclaurin (exp_R,].(- r),r.[,x)) . xx )
by FUNCT_1:def 3;
reconsider nn =
xx as
Element of
NAT by A1;
r = (x |^ nn) / (nn !)
by A1, TAYLOR_2:8, A0;
hence
0 < r
by A0;
verum
end;
hence
Maclaurin (exp_R,].(- r),r.[,x) is positive-yielding
by PARTFUN3:def 1; verum