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 A1: ( Z c= dom f & 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
A4: a < b and
A5: ( [.a,b.] c= Z & ((diff f,Z) . n) | [.a,b.] is continuous & 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) ! )) )
b - a <> 0 by A4;
then A6: (b - a) |^ (n + 1) <> 0 by CARD_4:51;
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
A7: 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;
A8: ((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 A6, XCMPLX_1:50, XCMPLX_1:88
.= 0 ;
then A9: g . a = 0 by A7;
A10: dom g = REAL by FUNCT_2:def 1;
then A11: g | [.a,b.] is continuous by A1, A4, A5, A7, A8, Th25;
( g is_differentiable_on ].a,b.[ & g . b = 0 ) by A1, A4, A5, A7, A8, A10, Th25;
then consider c being Real such that
A12: c in ].a,b.[ and
A13: diff g,c = 0 by A4, A10, A9, A11, ROLLE:1;
c in { r where r is Real : ( a < r & r < b ) } by A12, RCOMP_1:def 2;
then ex r being Real st
( c = r & a < r & r < b ) ;
then b - c <> 0 ;
then A14: (b - c) |^ n <> 0 by CARD_4:51;
dom g = REAL by FUNCT_2:def 1;
then (- (((((diff f,].a,b.[) . (n + 1)) . c) * ((b - c) |^ n)) / (n ! ))) + ((l * ((b - c) |^ n)) / (n ! )) = 0 by A1, A4, A5, A7, A8, A12, A13, Th25;
then ((((((diff f,].a,b.[) . (n + 1)) . c) * ((b - c) |^ n)) / (n ! )) * (n ! )) - (((l * ((b - c) |^ n)) / (n ! )) * (n ! )) = 0 ;
then ((((diff f,].a,b.[) . (n + 1)) . c) * ((b - c) |^ n)) - (((l * ((b - c) |^ n)) / (n ! )) * (n ! )) = 0 by 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 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 A14, 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 A8, A14, 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 A12; :: thesis: verum