let n be 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
A2: a < b and
A3: ( [.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 A2;
then A4: (b - a) |^ (n + 1) <> 0 by CARD_4:3;
deffunc H₁( Real) -> Element of REAL = In (((f . b) - ((Partial_Sums (Taylor (f,Z,$1,b))) . n)),REAL);
reconsider l = H₁(a) / (((b - a) |^ (n + 1)) / ((n + 1) !)) as Real ;
consider g being Function of REAL,REAL such that
A5: 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;
A6: ((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:74
.= H₁(a) - H₁(a) by A4, XCMPLX_1:50, XCMPLX_1:87
.= 0 ;
then A7: g . a = 0 by A5;
A8: dom g = REAL by FUNCT_2:def 1;
then A9: g | [.a,b.] is continuous by A1, A2, A3, A5, A6, Th25;
( g is_differentiable_on ].a,b.[ & g . b = 0 ) by A1, A2, A3, A5, A6, A8, Th25;
then consider c being Real such that
A10: c in ].a,b.[ and
A11: diff (g,c) = 0 by A2, A8, A7, A9, ROLLE:1;
c in { r where r is Real : ( a < r & r < b ) } by A10, RCOMP_1:def 2;
then ex r being Real st
( c = r & a < r & r < b ) ;
then b - c <> 0 ;
then A12: (b - c) |^ n <> 0 by CARD_4:3;
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, A2, A3, A5, A6, A10, A11, 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:87;
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:87;
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:120;
then (((diff (f,].a,b.[)) . (n + 1)) . c) - ((l * ((b - c) |^ n)) / ((b - c) |^ n)) = 0 by A12, XCMPLX_1:89;
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 A6, A12, XCMPLX_1:89;
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