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 . a = ((Partial_Sums (Taylor f,Z,b,a)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - b) |^ (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 . a = ((Partial_Sums (Taylor f,Z,b,a)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - b) |^ (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 . a = ((Partial_Sums (Taylor f,Z,b,a)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - b) |^ (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 . a = ((Partial_Sums (Taylor f,Z,b,a)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) ! )) )
A2: (n + 1) ! <> 0 by NEWTON:23;
A3: n ! <> 0 by NEWTON:23;
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 . a = ((Partial_Sums (Taylor f,Z,b,a)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - b) |^ (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 . a = ((Partial_Sums (Taylor f,Z,b,a)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) ! )) )
a - b <> 0 by A4;
then A6: (a - b) |^ (n + 1) <> 0 by CARD_4:51;
deffunc H₁( Real) -> Element of REAL = (f . a) - ((Partial_Sums (Taylor f,Z,$1,a)) . n);
reconsider l = H₁(b) / (((a - b) |^ (n + 1)) / ((n + 1) ! )) as Real ;
consider g being Function of REAL ,REAL such that
A7: for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) ! )) by Th26;
A8: ((f . a) - ((Partial_Sums (Taylor f,Z,b,a)) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) ! )) = H₁(b) - ((H₁(b) / (((a - b) |^ (n + 1)) / ((n + 1) ! ))) * (((a - b) |^ (n + 1)) / ((n + 1) ! ))) by XCMPLX_1:75
.= H₁(b) - H₁(b) by A6, A2, XCMPLX_1:50, XCMPLX_1:88
.= 0 ;
then A9: g . b = 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, Th28;
( g is_differentiable_on ].a,b.[ & g . a = 0 ) by A1, A4, A5, A7, A8, A10, Th28;
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 a - c <> 0 ;
then A14: (a - c) |^ n <> 0 by CARD_4:51;
dom g = REAL by FUNCT_2:def 1;
then (- (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - c) |^ n)) / (n ! ))) + ((l * ((a - c) |^ n)) / (n ! )) = 0 by A1, A4, A5, A7, A8, A12, A13, Th28;
then ((((((diff f,].a,b.[) . (n + 1)) . c) * ((a - c) |^ n)) / (n ! )) * (n ! )) - (((l * ((a - c) |^ n)) / (n ! )) * (n ! )) = 0 ;
then ((((diff f,].a,b.[) . (n + 1)) . c) * ((a - c) |^ n)) - (((l * ((a - c) |^ n)) / (n ! )) * (n ! )) = 0 by A3, XCMPLX_1:88;
then (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - c) |^ n)) - (l * ((a - c) |^ n))) / ((a - c) |^ n) = 0 / ((a - c) |^ n) by A3, XCMPLX_1:88;
then (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - c) |^ n)) / ((a - c) |^ n)) - ((l * ((a - c) |^ n)) / ((a - c) |^ n)) = 0 by XCMPLX_1:121;
then (((diff f,].a,b.[) . (n + 1)) . c) - ((l * ((a - c) |^ n)) / ((a - c) |^ n)) = 0 by A14, XCMPLX_1:90;
then ((diff f,].a,b.[) . (n + 1)) . c = l by A14, XCMPLX_1:90;
then f . a = (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) ! )) + ((Partial_Sums (Taylor f,Z,b,a)) . n) by A8;
hence ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor f,Z,b,a)) . n) + (((((diff f,].a,b.[) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) ! )) ) by A12; :: thesis: verum