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