let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL st Z c= dom f holds
for n being Nat st 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
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) )
let Z be Subset of REAL; :: thesis: ( Z c= dom f implies for n being Nat st 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
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) )
assume A1: Z c= dom f ; :: thesis: for n being Nat st 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
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) )
defpred S1[ Nat] means ( f is_differentiable_on $1,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . $1) | [.a,b.] is continuous & f is_differentiable_on $1 + 1,].a,b.[ holds
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . $1) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . ($1 + 1)) . x) * ((a - x) |^ $1)) / ($1 !)) ) ) );
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
assume A4: f is_differentiable_on k + 1,Z ; :: thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous & f is_differentiable_on (k + 1) + 1,].a,b.[ holds
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) )
let a, b be Real; :: thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous & f is_differentiable_on (k + 1) + 1,].a,b.[ implies for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) )
assume that
A5: a < b and
A6: [.a,b.] c= Z and
A7: ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous and
A8: f is_differentiable_on (k + 1) + 1,].a,b.[ ; :: thesis: for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) )
(diff (f,Z)) . k is_differentiable_on Z by A4;
then ((diff (f,Z)) . k) | Z is continuous by FDIFF_1:25;
then A9: ((diff (f,Z)) . k) | [.a,b.] is continuous by A6, FCONT_1:16;
A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A11: ].a,b.[ c= Z by A6, XBOOLE_1:1;
consider gk being PartFunc of REAL,REAL such that
A12: dom gk = Z and
A13: for x being Real st x in Z holds
gk . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . k) by Lm7;
A14: f is_differentiable_on k + 1,].a,b.[ by A8, Th23, NAT_1:11;
then A15: gk is_differentiable_on ].a,b.[ by A3, A4, A5, A6, A9, A12, A13, Th23, NAT_1:11;
A16: gk | [.a,b.] is continuous by A3, A4, A5, A6, A9, A14, A12, A13, Th23, NAT_1:11;
now :: thesis: for gk1 being PartFunc of REAL,REAL st dom gk1 = Z & ( for x being Real st x in Z holds
gk1 . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds
( gk1 . a = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) )
A17: (diff (f,Z)) . k is_differentiable_on Z by A4;
k <= ((k + 1) + 1) - 1 by NAT_1:11;
then A18: (diff (f,].a,b.[)) . k is_differentiable_on ].a,b.[ by A8;
A19: (diff (f,Z)) . (k + 1) = ((diff (f,Z)) . k) `| Z by Def5;
let gk1 be PartFunc of REAL,REAL; :: thesis: ( dom gk1 = Z & ( for x being Real st x in Z holds
gk1 . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) implies ( gk1 . a = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) )
assume that
A20: dom gk1 = Z and
A21: for x being Real st x in Z holds
gk1 . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ; :: thesis: ( gk1 . a = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) )
A22: a in [.a,b.] by A5, XXREAL_1:1;
then gk1 . a = (f . a) - ((Partial_Sums (Taylor (f,Z,a,a))) . (k + 1)) by A6, A21
.= (f . a) - (((Partial_Sums (Taylor (f,Z,a,a))) . k) + ((Taylor (f,Z,a,a)) . (k + 1))) by SERIES_1:def 1
.= ((f . a) - ((Partial_Sums (Taylor (f,Z,a,a))) . k)) - ((Taylor (f,Z,a,a)) . (k + 1))
.= (gk . a) - ((Taylor (f,Z,a,a)) . (k + 1)) by A6, A13, A22
.= 0 - ((Taylor (f,Z,a,a)) . (k + 1)) by A3, A4, A5, A6, A9, A14, A12, A13, Th23, NAT_1:11
.= 0 - (((((diff (f,Z)) . (k + 1)) . a) * ((a - a) |^ (k + 1))) / ((k + 1) !)) by Def7
.= 0 - (((((diff (f,Z)) . (k + 1)) . a) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6
.= 0 ;
hence gk1 . a = 0 ; :: thesis: ( gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) )
consider h being PartFunc of REAL,REAL such that
A23: dom h = [#] REAL and
A24: for x being Real holds h . x = (1 * ((a - x) |^ (k + 1))) / ((k + 1) !) and
A25: for x being Real holds
( h is_differentiable_in x & diff (h,x) = - ((1 * ((a - x) |^ k)) / (k !)) ) by Lm6;
A26: dom (((diff (f,Z)) . (k + 1)) (#) h) = (dom ((diff (f,Z)) . (k + 1))) /\ (dom h) by VALUED_1:def 4
.= Z /\ REAL by A23, A19, A17, FDIFF_1:def 7
.= Z by XBOOLE_1:28 ;
A27: dom (gk - (((diff (f,Z)) . (k + 1)) (#) h)) = (dom gk) /\ (dom (((diff (f,Z)) . (k + 1)) (#) h)) by VALUED_1:12
.= Z by A12, A26 ;
thus gk1 | [.a,b.] is continuous :: thesis: ( gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) )
proof
set ghk = gk - (((diff (f,Z)) . (k + 1)) (#) h);
for x being Real st x in REAL holds
h is_differentiable_in x by A25;
then h is_differentiable_on REAL by A23, FDIFF_1:9;
then h | REAL is continuous by FDIFF_1:25;
then A28: h | [.a,b.] is continuous by FCONT_1:16;
now :: thesis: for x being Element of REAL st x in Z holds
gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x
let x be Element of REAL ; :: thesis: ( x in Z implies gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x )
assume A29: x in Z ; :: thesis: gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x
thus gk1 . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) by A21, A29
.= (f . a) - (((Partial_Sums (Taylor (f,Z,x,a))) . k) + ((Taylor (f,Z,x,a)) . (k + 1))) by SERIES_1:def 1
.= ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . k)) - ((Taylor (f,Z,x,a)) . (k + 1))
.= (gk . x) - ((Taylor (f,Z,x,a)) . (k + 1)) by A13, A29
.= (gk . x) - (((((diff (f,Z)) . (k + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) by Def7
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * ((1 * ((a - x) |^ (k + 1))) / ((k + 1) !))) by XCMPLX_1:74
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A24
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A27, A29, VALUED_1:13 ; :: thesis: verum
end;
then A30: gk1 = gk - (((diff (f,Z)) . (k + 1)) (#) h) by A20, A27, PARTFUN1:5;
[.a,b.] c= dom ((diff (f,Z)) . (k + 1)) by A6, A19, A17, FDIFF_1:def 7;
then (((diff (f,Z)) . (k + 1)) (#) h) | ([.a,b.] /\ [.a,b.]) is continuous by A7, A23, A28, FCONT_1:19;
hence gk1 | [.a,b.] is continuous by A6, A12, A16, A26, A30, FCONT_1:19; :: thesis: verum
end;
A31: (diff (f,].a,b.[)) . (k + 1) = ((diff (f,].a,b.[)) . k) `| ].a,b.[ by Def5;
set gfh = gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h);
A32: dom (((diff (f,].a,b.[)) . (k + 1)) (#) h) = (dom ((diff (f,].a,b.[)) . (k + 1))) /\ (dom h) by VALUED_1:def 4
.= ].a,b.[ /\ REAL by A23, A31, A18, FDIFF_1:def 7
.= ].a,b.[ by XBOOLE_1:28 ;
A33: dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = Z /\ (dom (((diff (f,].a,b.[)) . (k + 1)) (#) h)) by A12, VALUED_1:12
.= ].a,b.[ by A6, A10, A32, XBOOLE_1:1, XBOOLE_1:28 ;
A34: for x being Real st x in ].a,b.[ holds
(gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x
proof
let x be Real; :: thesis: ( x in ].a,b.[ implies (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x )
assume A35: x in ].a,b.[ ; :: thesis: (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x
thus (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x = (gk . x) - ((((diff (f,].a,b.[)) . (k + 1)) (#) h) . x) by A33, A35, VALUED_1:13
.= (gk . x) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (h . x)) by VALUED_1:5
.= (gk . x) - (((((diff (f,Z)) . (k + 1)) | ].a,b.[) . x) * (h . x)) by A4, A5, A6, A10, Th24, XBOOLE_1:1
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A35, FUNCT_1:49
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A11, A27, A35, VALUED_1:13 ; :: thesis: verum
end;
A36: now :: thesis: for xx being object st xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) holds
gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx
let xx be object ; :: thesis: ( xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) implies gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx )
assume A37: xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) ; :: thesis: gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx
reconsider x = xx as Real by A37;
thus gk1 . xx = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) by A11, A21, A33, A37
.= (f . a) - (((Partial_Sums (Taylor (f,Z,x,a))) . k) + ((Taylor (f,Z,x,a)) . (k + 1))) by SERIES_1:def 1
.= ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . k)) - ((Taylor (f,Z,x,a)) . (k + 1))
.= (gk . x) - ((Taylor (f,Z,x,a)) . (k + 1)) by A11, A13, A33, A37
.= (gk . x) - (((((diff (f,Z)) . (k + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) by Def7
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * ((1 * ((a - x) |^ (k + 1))) / ((k + 1) !))) by XCMPLX_1:74
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A24
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A11, A27, A33, A37, VALUED_1:13
.= (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx by A33, A34, A37 ; :: thesis: verum
end;
A38: (diff (f,].a,b.[)) . (k + 1) is_differentiable_on ].a,b.[ by A8;
for x being Real st x in ].a,b.[ holds
h is_differentiable_in x by A25;
then A39: h is_differentiable_on ].a,b.[ by A23, FDIFF_1:9;
then A40: ((diff (f,].a,b.[)) . (k + 1)) (#) h is_differentiable_on ].a,b.[ by A32, A38, FDIFF_1:21;
then A41: gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h) is_differentiable_on ].a,b.[ by A15, A33, FDIFF_1:19;
dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = (dom gk1) /\ ].a,b.[ by A6, A10, A20, A33, XBOOLE_1:1, XBOOLE_1:28;
then A42: (gk1 | ].a,b.[) | ].a,b.[ = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ by A36, FUNCT_1:46;
then (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ = gk1 | ].a,b.[ by FUNCT_1:51;
then for x being Real st x in ].a,b.[ holds
gk1 | ].a,b.[ is_differentiable_in x by A41, FDIFF_1:def 6;
hence A43: gk1 is_differentiable_on ].a,b.[ by A11, A20, FDIFF_1:def 6; :: thesis: for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !))
now :: thesis: for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !))
let x be Real; :: thesis: ( x in ].a,b.[ implies diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) )
assume A44: x in ].a,b.[ ; :: thesis: diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !))
thus diff (gk1,x) = (gk1 `| ].a,b.[) . x by A43, A44, FDIFF_1:def 7
.= ((gk1 | ].a,b.[) `| ].a,b.[) . x by A43, FDIFF_2:16
.= (((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[) `| ].a,b.[) . x by A42, FUNCT_1:51
.= ((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) `| ].a,b.[) . x by A41, FDIFF_2:16
.= (diff (gk,x)) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A15, A33, A40, A44, FDIFF_1:19
.= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A3, A4, A5, A6, A9, A14, A12, A13, A44, Th23, NAT_1:11
.= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (((((diff (f,].a,b.[)) . (k + 1)) (#) h) `| ].a,b.[) . x) by A40, A44, FDIFF_1:def 7
.= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (((h . x) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) + ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x)))) by A32, A38, A39, A44, FDIFF_1:21
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - ((h . x) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x)))
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (((1 * ((a - x) |^ (k + 1))) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x))) by A24
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (- ((1 * ((a - x) |^ k)) / (k !)))) by A25
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) + ((((diff (f,].a,b.[)) . (k + 1)) . x) * ((1 * ((a - x) |^ k)) / (k !)))) - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) + (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) by XCMPLX_1:74
.= - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))
.= - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * ((((diff (f,].a,b.[)) . (k + 1)) `| ].a,b.[) . x)) by A38, A44, FDIFF_1:def 7
.= - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (((diff (f,].a,b.[)) . ((k + 1) + 1)) . x)) by Def5
.= - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) by XCMPLX_1:74 ; :: thesis: verum
end;
hence for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ; :: thesis: verum
end;
hence for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) ; :: thesis: verum
end;
A45: S1[ 0 ]
proof
assume f is_differentiable_on 0 ,Z ; :: thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . 0) | [.a,b.] is continuous & f is_differentiable_on 0 + 1,].a,b.[ holds
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) )
let a, b be Real; :: thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . 0) | [.a,b.] is continuous & f is_differentiable_on 0 + 1,].a,b.[ implies for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) )
assume that
A46: a < b and
A47: [.a,b.] c= Z and
A48: ((diff (f,Z)) . 0) | [.a,b.] is continuous and
A49: f is_differentiable_on 0 + 1,].a,b.[ ; :: thesis: for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) )
A50: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A51: ].a,b.[ c= Z by A47, XBOOLE_1:1;
let g be PartFunc of REAL,REAL; :: thesis: ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ) implies ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) )
assume that
A52: dom g = Z and
A53: for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ; :: thesis: ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) )
A54: a in [.a,b.] by A46, XXREAL_1:1;
hence g . a = (f . a) - ((Partial_Sums (Taylor (f,Z,a,a))) . 0) by A47, A53
.= (f . a) - ((Taylor (f,Z,a,a)) . 0) by SERIES_1:def 1
.= (f . a) - (((((diff (f,Z)) . 0) . a) * ((a - a) |^ 0)) / (0 !)) by Def7
.= (f . a) - ((((f | Z) . a) * ((a - a) |^ 0)) / (0 !)) by Def5
.= (f . a) - (((f . a) * ((a - a) |^ 0)) / (0 !)) by A47, A54, FUNCT_1:49
.= (f . a) - ((f . a) * 1) by NEWTON:4, NEWTON:12
.= 0 ;
:: thesis: ( g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) )
consider y being PartFunc of REAL,REAL such that
A55: dom y = [#] REAL and
A56: for x being Real holds y . x = (f . a) - x and
A57: for x being Real holds
( y is_differentiable_in x & diff (y,x) = - 1 ) by Lm5;
rng f c= REAL ;
then A58: dom (y * f) = dom f by A55, RELAT_1:27;
for x being Real st x in REAL holds
y is_differentiable_in x by A57;
then y is_differentiable_on REAL by A55, FDIFF_1:9;
then y | REAL is continuous by FDIFF_1:25;
then A59: y | (f .: [.a,b.]) is continuous by FCONT_1:16;
rng f c= dom y by A55;
then A60: dom (y * f) = dom f by RELAT_1:27;
A61: [.a,b.] c= dom f by A1, A47, XBOOLE_1:1;
then A62: ].a,b.[ c= dom f by A50, XBOOLE_1:1;
(diff (f,].a,b.[)) . 0 is_differentiable_on ].a,b.[ by A49;
then f | ].a,b.[ is_differentiable_on ].a,b.[ by Def5;
then for x being Real st x in ].a,b.[ holds
f | ].a,b.[ is_differentiable_in x by FDIFF_1:9;
then A63: f is_differentiable_on ].a,b.[ by A62, FDIFF_1:def 6;
A64: for x being Real st x in ].a,b.[ holds
( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) )
proof
A65: (diff (f,].a,b.[)) . (0 + 1) = ((diff (f,].a,b.[)) . 0) `| ].a,b.[ by Def5
.= (f | ].a,b.[) `| ].a,b.[ by Def5
.= f `| ].a,b.[ by A63, FDIFF_2:16 ;
let x be Real; :: thesis: ( x in ].a,b.[ implies ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) )
assume A66: x in ].a,b.[ ; :: thesis: ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) )
A67: f is_differentiable_in x by A63, A66, FDIFF_1:9;
A68: y is_differentiable_in f . x by A57;
hence y * f is_differentiable_in x by A67, FDIFF_2:13; :: thesis: diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !))
A69: ((a - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12;
thus diff ((y * f),x) = (diff (y,(f . x))) * (diff (f,x)) by A68, A67, FDIFF_2:13
.= (diff (y,(f . x))) * ((f `| ].a,b.[) . x) by A63, A66, FDIFF_1:def 7
.= (- 1) * (((diff (f,].a,b.[)) . (0 + 1)) . x) by A57, A65
.= - ((((diff (f,].a,b.[)) . (0 + 1)) . x) * (((a - x) |^ 0) / (0 !))) by A69
.= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) by XCMPLX_1:74 ; :: thesis: verum
end;
then for x being Real st x in ].a,b.[ holds
y * f is_differentiable_in x ;
then A70: y * f is_differentiable_on ].a,b.[ by A62, A60, FDIFF_1:9;
A71: dom ((y * f) | [.a,b.]) = (dom (y * f)) /\ [.a,b.] by RELAT_1:61
.= [.a,b.] by A1, A47, A58, XBOOLE_1:1, XBOOLE_1:28
.= Z /\ [.a,b.] by A47, XBOOLE_1:28
.= dom (g | [.a,b.]) by A52, RELAT_1:61 ;
A72: now :: thesis: for xx being object st xx in dom (g | [.a,b.]) holds
(g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx
let xx be object ; :: thesis: ( xx in dom (g | [.a,b.]) implies (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx )
assume A73: xx in dom (g | [.a,b.]) ; :: thesis: (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx
reconsider x = xx as Real by A73;
dom (g | [.a,b.]) = (dom g) /\ [.a,b.] by RELAT_1:61;
then dom (g | [.a,b.]) c= [.a,b.] by XBOOLE_1:17;
then A74: x in [.a,b.] by A73;
thus (g | [.a,b.]) . xx = g . x by A73, FUNCT_1:47
.= (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) by A47, A53, A74
.= (f . a) - ((Taylor (f,Z,x,a)) . 0) by SERIES_1:def 1
.= (f . a) - (((((diff (f,Z)) . 0) . x) * ((a - x) |^ 0)) / (0 !)) by Def7
.= (f . a) - ((((f | Z) . x) * ((a - x) |^ 0)) / (0 !)) by Def5
.= (f . a) - (((f . x) * ((a - x) |^ 0)) / (0 !)) by A47, A74, FUNCT_1:49
.= (f . a) - ((f . x) * 1) by NEWTON:4, NEWTON:12
.= y . (f . x) by A56
.= (y * f) . x by A61, A74, FUNCT_1:13
.= ((y * f) | [.a,b.]) . xx by A71, A73, FUNCT_1:47 ; :: thesis: verum
end;
(f | Z) | [.a,b.] is continuous by A48, Def5;
then ((f | Z) | [.a,b.]) | [.a,b.] is continuous by FCONT_1:15;
then (f | [.a,b.]) | [.a,b.] is continuous by A47, FUNCT_1:51;
then f | [.a,b.] is continuous by FCONT_1:15;
then (y * f) | [.a,b.] is continuous by A59, FCONT_1:25;
hence g | [.a,b.] is continuous by A71, A72, FUNCT_1:2; :: thesis: ( g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) )
A75: dom ((y * f) | ].a,b.[) = (dom (y * f)) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A50, A61, A60, XBOOLE_1:1, XBOOLE_1:28
.= Z /\ ].a,b.[ by A47, A50, XBOOLE_1:1, XBOOLE_1:28
.= dom (g | ].a,b.[) by A52, RELAT_1:61 ;
now :: thesis: for xx being object st xx in dom (g | ].a,b.[) holds
(g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx
let xx be object ; :: thesis: ( xx in dom (g | ].a,b.[) implies (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx )
assume A76: xx in dom (g | ].a,b.[) ; :: thesis: (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx
reconsider x = xx as Real by A76;
dom (g | ].a,b.[) = (dom g) /\ ].a,b.[ by RELAT_1:61;
then dom (g | ].a,b.[) c= ].a,b.[ by XBOOLE_1:17;
then A77: x in ].a,b.[ by A76;
A78: ((a - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12;
thus (g | ].a,b.[) . xx = g . x by A76, FUNCT_1:47
.= (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) by A53, A51, A77
.= (f . a) - ((Taylor (f,Z,x,a)) . 0) by SERIES_1:def 1
.= (f . a) - (((((diff (f,Z)) . 0) . x) * ((a - x) |^ 0)) / (0 !)) by Def7
.= (f . a) - ((((f | Z) . x) * ((a - x) |^ 0)) / (0 !)) by Def5
.= (f . a) - (((f . x) * ((a - x) |^ 0)) / (0 !)) by A51, A77, FUNCT_1:49
.= (f . a) - ((f . x) * (((a - x) |^ 0) / (0 !))) by XCMPLX_1:74
.= y . (f . x) by A56, A78
.= (y * f) . x by A62, A77, FUNCT_1:13
.= ((y * f) | ].a,b.[) . xx by A75, A76, FUNCT_1:47 ; :: thesis: verum
end;
then A79: g | ].a,b.[ = (y * f) | ].a,b.[ by A75, FUNCT_1:2;
then g | ].a,b.[ is_differentiable_on ].a,b.[ by A70, FDIFF_2:16;
then for x being Real st x in ].a,b.[ holds
g | ].a,b.[ is_differentiable_in x by FDIFF_1:9;
hence A80: g is_differentiable_on ].a,b.[ by A52, A51, FDIFF_1:def 6; :: thesis: for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !))
now :: thesis: for x being Real st x in ].a,b.[ holds
( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) )
let x be Real; :: thesis: ( x in ].a,b.[ implies ( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) )
assume A81: x in ].a,b.[ ; :: thesis: ( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) )
thus g is_differentiable_in x by A80, A81, FDIFF_1:9; :: thesis: diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !))
thus diff (g,x) = (g `| ].a,b.[) . x by A80, A81, FDIFF_1:def 7
.= ((g | ].a,b.[) `| ].a,b.[) . x by A80, FDIFF_2:16
.= ((y * f) `| ].a,b.[) . x by A79, A70, FDIFF_2:16
.= diff ((y * f),x) by A70, A81, FDIFF_1:def 7
.= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) by A64, A81 ; :: thesis: verum
end;
hence for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A45, A2);
 hence for n being Nat st 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
for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds
( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) ; :: thesis: verum