let n be Nat; 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; 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; ( 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 )
; 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 a, b be Real; ( 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
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.[ )
; 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) !)) )
reconsider aa = a, bb = b as Real ;
a - b <> 0
by A2;
then A4:
(a - b) |^ (n + 1) <> 0
by CARD_4:3;
deffunc H1( Real) -> Element of REAL = In (((f . a) - ((Partial_Sums (Taylor (f,Z,$1,a))) . n)),REAL);
reconsider l = H1(bb) / (((a - b) |^ (n + 1)) / ((n + 1) !)) as Real ;
consider g being Function of REAL,REAL such that
A5:
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;
A6: ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) =
H1(bb) - ((H1(bb) / (((a - b) |^ (n + 1)) / ((n + 1) !))) * (((a - b) |^ (n + 1)) / ((n + 1) !)))
by XCMPLX_1:74
.=
H1(bb) - H1(bb)
by A4, XCMPLX_1:50, XCMPLX_1:87
.=
0
;
then A7:
g . b = 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, Th28;
( g is_differentiable_on ].a,b.[ & g . a = 0 )
by A1, A2, A3, A5, A6, A8, Th28;
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
a - c <> 0
;
then A12:
(a - c) |^ n <> 0
by CARD_4:3;
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, A2, A3, A5, A6, A10, A11, 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 XCMPLX_1:87;
then
(((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) - (l * ((a - c) |^ n))) / ((a - c) |^ n) = 0 / ((a - c) |^ n)
by XCMPLX_1:87;
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:120;
then
(((diff (f,].a,b.[)) . (n + 1)) . c) - ((l * ((a - c) |^ n)) / ((a - c) |^ n)) = 0
by A12, XCMPLX_1:89;
then
((diff (f,].a,b.[)) . (n + 1)) . c = l
by A12, XCMPLX_1:89;
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 A6;
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 A10; verum