let n be Element of NAT ; :: thesis: for f being PartFunc of REAL ,REAL
for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & ((diff f,Z) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor f,Z,a,b)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) )
let f be PartFunc of REAL ,REAL ; :: thesis: for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & ((diff f,Z) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor f,Z,a,b)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) )
let Z be Subset of REAL ; :: thesis: ( Z c= dom f & f is_differentiable_on n,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff f,Z) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor f,Z,a,b)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) ) )
assume that
A0: Z c= dom f and
A1: f is_differentiable_on n,Z ; :: thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff f,Z) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor f,Z,a,b)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) )
let a, b be Real; :: thesis: ( a < b & [.a,b.] c= Z & ((diff f,Z) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor f,Z,a,b)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) ) )
assume that
A2: a < b and
A3: [.a,b.] c= Z and
A4: ((diff f,Z) . n) | [.a,b.] is continuous and
A5: f is_differentiable_on n + 1,].a,b.[ ; :: thesis: ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor f,Z,a,b)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) )
deffunc H₁( Real) -> Element of REAL = (f . b) - ((Partial_Sums (Taylor f,Z,$1,b)) . n);
reconsider l = H₁(a) / (((b - a) |^ (n + 1)) / ((n + 1) ! )) as Real ;
consider g being Function of REAL ,REAL such that
A6: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor f,Z,x,b)) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! )) by Th26;
b - a <> 0 by A2;
then A7: (b - a) |^ (n + 1) <> 0 by CARD_4:51;
A8: (n + 1) ! <> 0 by NEWTON:23;
A9: ((f . b) - ((Partial_Sums (Taylor f,Z,a,b)) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) ! )) = H₁(a) - ((H₁(a) / (((b - a) |^ (n + 1)) / ((n + 1) ! ))) * (((b - a) |^ (n + 1)) / ((n + 1) ! ))) by XCMPLX_1:75
.= H₁(a) - H₁(a) by A7, A8, XCMPLX_1:50, XCMPLX_1:88
.= 0 ;
X: dom g = REAL by FUNCT_2:def 1;
then Y: [.a,b.] c= dom g ;
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff g,x = (- (((((diff f,].a,b.[) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) + ((l * ((b - x) |^ n)) / (n ! )) ) ) by A1, A2, A3, A4, A5, A6, A9, Th25, A0, X;
then consider c being Real such that
A10: c in ].a,b.[ and
A11: diff g,c = 0 by A2, Y, ROLLE:1;
dom g = REAL by FUNCT_2:def 1;
then A12: (- (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - c) |^ n)) / (n ! ))) + ((l * ((b - c) |^ n)) / (n ! )) = 0 by A1, A2, A3, A4, A5, A6, A9, A10, A11, Th25, A0;
A13: n ! <> 0 by NEWTON:23;
c in { r where r is Real : ( a < r & r < b ) } by A10, RCOMP_1:def 2;
then consider r being Real such that
A14: ( c = r & a < r & r < b ) ;
b - c <> 0 by A14;
then A15: (b - c) |^ n <> 0 by CARD_4:51;
((((((diff f,].a,b.[) . (n + 1)) . c) * ((b - c) |^ n)) / (n ! )) * (n ! )) - (((l * ((b - c) |^ n)) / (n ! )) * (n ! )) = 0 by A12;
then ((((diff f,].a,b.[) . (n + 1)) . c) * ((b - c) |^ n)) - (((l * ((b - c) |^ n)) / (n ! )) * (n ! )) = 0 by A13, XCMPLX_1:88;
then (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - c) |^ n)) - (l * ((b - c) |^ n))) / ((b - c) |^ n) = 0 / ((b - c) |^ n) by A13, XCMPLX_1:88;
then (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - c) |^ n)) / ((b - c) |^ n)) - ((l * ((b - c) |^ n)) / ((b - c) |^ n)) = 0 by XCMPLX_1:121;
then (((diff f,].a,b.[) . (n + 1)) . c) - ((l * ((b - c) |^ n)) / ((b - c) |^ n)) = 0 by A15, XCMPLX_1:90;
then ((f . b) - ((Partial_Sums (Taylor f,Z,a,b)) . n)) - (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) = 0 by A9, A15, XCMPLX_1:90;
then f . b = (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) + ((Partial_Sums (Taylor f,Z,a,b)) . n) ;
hence ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor f,Z,a,b)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) ) by A10; :: thesis: verum