defpred S1[ set ] means $1 in REAL ;
let n be Nat; :: thesis: for l, b being Real ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) )
let l, b be Real; :: thesis: ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) )
deffunc H1( Real) -> Element of REAL = In (((l * ((b - $1) |^ (n + 1))) / ((n + 1) !)),REAL);
consider g being PartFunc of REAL,REAL such that
A1: for d being Element of REAL holds
( d in dom g iff S1[d] ) and
A2: for d being Element of REAL st d in dom g holds
g /. d = H1(d) from PARTFUN2:sch 2();
 take g ; :: thesis: ( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) )
consider f being PartFunc of REAL,REAL such that
A3: dom f = [#] REAL and
A4: for x being Real holds f . x = b - x and
A5: for x being Real holds
( f is_differentiable_in x & diff (f,x) = - 1 ) by Lm5;
( dom (#Z (n + 1)) = REAL & rng f c= REAL ) by FUNCT_2:def 1;
then A6: dom ((#Z (n + 1)) * f) = dom f by RELAT_1:27;
for x being object st x in REAL holds
x in dom g by A1;
then A7: REAL c= dom g by TARSKI:def 3;
then A8: dom g = [#] REAL by XBOOLE_0:def 10;
A9: for d being Real holds g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !)
proof
let d be Real; :: thesis: g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !)
reconsider d = d as Element of REAL by XREAL_0:def 1;
g /. d = H1(d) by A2, A8;
hence g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) by A8, PARTFUN1:def 6; :: thesis: verum
end;
A10: now :: thesis: for x being Element of REAL st x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) holds
((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x
let x be Element of REAL ; :: thesis: ( x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) implies ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x )
assume x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) ; :: thesis: ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x
hence ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = (l / ((n + 1) !)) * (((#Z (n + 1)) * f) . x) by VALUED_1:def 5
.= (l / ((n + 1) !)) * (((#Z (n + 1)) * f) /. x) by A3, A6, PARTFUN1:def 6
.= (l / ((n + 1) !)) * ((#Z (n + 1)) /. (f /. x)) by A3, A6, PARTFUN2:3
.= (l / ((n + 1) !)) * ((#Z (n + 1)) . (f . x)) by A3, PARTFUN1:def 6
.= (l / ((n + 1) !)) * ((f . x) #Z (n + 1)) by Def1
.= (l / ((n + 1) !)) * ((f . x) |^ (n + 1)) by PREPOWER:36
.= (l / ((n + 1) !)) * ((b - x) |^ (n + 1)) by A4
.= (l * ((b - x) |^ (n + 1))) / ((n + 1) !) by XCMPLX_1:74
.= g . x by A9 ;
:: thesis: verum
end;
A11: for x being Real holds
( (#Z (n + 1)) * f is_differentiable_in x & diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) )
proof
let xx be Real; :: thesis: ( (#Z (n + 1)) * f is_differentiable_in xx & diff (((#Z (n + 1)) * f),xx) = - ((n + 1) * ((b - xx) #Z n)) )
reconsider x = xx as Real ;
A12: ( f is_differentiable_in x & #Z (n + 1) is_differentiable_in f . x ) by A5, Th2;
hence (#Z (n + 1)) * f is_differentiable_in xx by FDIFF_2:13; :: thesis: diff (((#Z (n + 1)) * f),xx) = - ((n + 1) * ((b - xx) #Z n))
diff ((#Z (n + 1)),(f . x)) = (n + 1) * ((f . x) #Z ((n + 1) - 1)) by Th2;
hence diff (((#Z (n + 1)) * f),xx) = ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (diff (f,x)) by A12, FDIFF_2:13
.= ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (- 1) by A5
.= ((n + 1) * ((b - x) #Z ((n + 1) - 1))) * (- 1) by A4
.= - ((n + 1) * ((b - xx) #Z n)) ;
:: thesis: verum
end;
A13: now :: thesis: for x being Real holds
( (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x & diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !)) )
let x be Real; :: thesis: ( (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x & diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !)) )
A14: (n + 1) / ((n + 1) !) = (1 * (n + 1)) / ((n !) * (n + 1)) by NEWTON:15
.= 1 / (n !) by XCMPLX_1:91 ;
A15: (#Z (n + 1)) * f is_differentiable_in x by A11;
hence (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x by FDIFF_1:15; :: thesis: diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !))
thus diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = (l / ((n + 1) !)) * (diff (((#Z (n + 1)) * f),x)) by A15, FDIFF_1:15
.= ((diff (((#Z (n + 1)) * f),x)) / ((n + 1) !)) * l by XCMPLX_1:75
.= l * ((- ((n + 1) * ((b - x) #Z n))) / ((n + 1) !)) by A11
.= l * ((- ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)) by PREPOWER:36
.= (l * (- ((n + 1) * ((b - x) |^ n)))) / ((n + 1) !) by XCMPLX_1:74
.= ((- l) * ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)
.= (- l) * (((n + 1) * ((b - x) |^ n)) / ((n + 1) !)) by XCMPLX_1:74
.= (- l) * (((b - x) |^ n) * ((n + 1) / ((n + 1) !))) by XCMPLX_1:74
.= (- l) * (((b - x) |^ n) / (n !)) by A14, XCMPLX_1:99
.= - (l * (((b - x) |^ n) / (n !)))
.= - ((l * ((b - x) |^ n)) / (n !)) by XCMPLX_1:74 ; :: thesis: verum
end;
dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) = dom g by A8, A3, A6, VALUED_1:def 5;
then (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) = g by A10, PARTFUN1:5;
hence ( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) by A7, A9, A13, XBOOLE_0:def 10; :: thesis: verum