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