let a be Real; for n being Nat
for g being Function of REAL,REAL st ( for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) )
let n be Nat; for g being Function of REAL,REAL st ( for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) )
let g be Function of REAL,REAL; ( ( for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ) implies for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) ) )
A1:
dom g = REAL
by FUNCT_2:def 1;
assume A2:
for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !)
; for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) )
defpred S1[ set ] means $1 in REAL ;
deffunc H1( Real) -> Element of REAL = In ((($1 - a) |^ (n + 1)),REAL);
consider f being PartFunc of REAL,REAL such that
A3:
for d being Element of REAL holds
( d in dom f iff S1[d] )
and
A4:
for d being Element of REAL st d in dom f holds
f /. d = H1(d)
from PARTFUN2:sch 2();
for x being object st x in REAL holds
x in dom f
by A3;
then
REAL c= dom f
by TARSKI:def 3;
then A5:
dom f = REAL
by XBOOLE_0:def 10;
A6:
for d being Real holds f . d = (d - a) |^ (n + 1)
A8:
f is Function of REAL,REAL
by A5, FUNCT_2:67;
A9:
dom ((1 / ((n + 1) !)) (#) f) = dom f
by VALUED_1:def 5;
A11:
for x being Real holds
( (1 / ((n + 1) !)) (#) f is_differentiable_in x & diff (((1 / ((n + 1) !)) (#) f),x) = ((x - a) |^ n) / (n !) )
proof
let x be
Real;
( (1 / ((n + 1) !)) (#) f is_differentiable_in x & diff (((1 / ((n + 1) !)) (#) f),x) = ((x - a) |^ n) / (n !) )
A12:
(n + 1) / ((n + 1) !) =
(1 * (n + 1)) / ((n !) * (n + 1))
by NEWTON:15
.=
1
/ (n !)
by XCMPLX_1:91
;
A13:
f is_differentiable_in x
by A8, A6, Th46;
hence
(1 / ((n + 1) !)) (#) f is_differentiable_in x
by FDIFF_1:15;
diff (((1 / ((n + 1) !)) (#) f),x) = ((x - a) |^ n) / (n !)
thus diff (
((1 / ((n + 1) !)) (#) f),
x) =
(1 / ((n + 1) !)) * (diff (f,x))
by A13, FDIFF_1:15
.=
((diff (f,x)) / ((n + 1) !)) * 1
by XCMPLX_1:75
.=
(1 * ((n + 1) * ((x - a) |^ n))) / ((n + 1) !)
by A8, A6, Th46
.=
1
* (((x - a) |^ n) * ((n + 1) / ((n + 1) !)))
by XCMPLX_1:74
.=
((x - a) |^ n) / (n !)
by A12, XCMPLX_1:99
;
verum
end;
(1 / ((n + 1) !)) (#) f = g
by A10, PARTFUN1:5, A1, A5, A9;
hence
for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) )
by A11; verum