let n be Nat; for f being PartFunc of REAL,REAL
for x0, r being Real st ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds
for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
let f be PartFunc of REAL,REAL; for x0, r being Real st ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds
for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
let x0, r be Real; ( ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ implies for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) )
assume that
A1:
].(x0 - r),(x0 + r).[ c= dom f
and
A2:
0 < r
and
A3:
f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[
; for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
let x be Real; ( x in ].(x0 - r),(x0 + r).[ implies ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) )
assume A4:
x in ].(x0 - r),(x0 + r).[
; ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
now ( ( x < x0 & ex s being set st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ) or ( x = x0 & ex s being set st
( 0 < s & s < 1 & ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x ) ) or ( x > x0 & ex s being set st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ) )per cases
( x < x0 or x = x0 or x > x0 )
by XXREAL_0:1;
case A5:
x < x0
;
ex s being set st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
|.(x0 - x0).| = 0
by ABSVALUE:2;
then
x0 in ].(x0 - r),(x0 + r).[
by A2, RCOMP_1:1;
then A6:
[.x,x0.] c= ].(x0 - r),(x0 + r).[
by A4, XXREAL_2:def 12;
(diff (f,].(x0 - r),(x0 + r).[)) . n is_differentiable_on ].(x0 - r),(x0 + r).[
by A3;
then
((diff (f,].(x0 - r),(x0 + r).[)) . n) | ].(x0 - r),(x0 + r).[ is
continuous
by FDIFF_1:25;
then A7:
((diff (f,].(x0 - r),(x0 + r).[)) . n) | [.x,x0.] is
continuous
by A6, FCONT_1:16;
A8:
f is_differentiable_on n,
].(x0 - r),(x0 + r).[
by A3, Th23, NAT_1:11;
set t =
x0 - x;
A9:
x0 - x > 0
by A5, XREAL_1:50;
A10:
].x,x0.[ c= [.x,x0.]
by XXREAL_1:25;
then
f is_differentiable_on n + 1,
].x,x0.[
by A3, A6, Th31, XBOOLE_1:1;
then consider c being
Real such that A11:
c in ].x,x0.[
and A12:
f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].x,x0.[)) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !))
by A1, A5, A6, A8, A7, Th29;
take s =
(x0 - c) / (x0 - x);
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )A13:
x0 + (s * (x - x0)) =
x0 - (((x0 - c) / (x0 - x)) * (x0 - x))
.=
x0 - (x0 - c)
by A9, XCMPLX_1:87
.=
c
;
c in { p where p is Real : ( x0 - (x0 - x) < p & p < x0 ) }
by A11, RCOMP_1:def 2;
then A14:
ex
g being
Real st
(
g = c &
x0 - (x0 - x) < g &
g < x0 )
;
then
0 < x0 - c
by XREAL_1:50;
then
0 / (x0 - x) < (x0 - c) / (x0 - x)
by A9, XREAL_1:74;
hence
0 < s
;
( s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
(x0 - (x0 - x)) + (x0 - x) < c + (x0 - x)
by A14, XREAL_1:8;
then
x0 - c < x0 - x
by XREAL_1:19;
then
(x0 - c) / (x0 - x) < (x0 - x) / (x0 - x)
by A9, XREAL_1:74;
hence
s < 1
by A9, XCMPLX_1:60;
f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !))((diff (f,].x,x0.[)) . (n + 1)) . c =
(((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) | ].x,x0.[) . c
by A3, A6, A10, Th30, XBOOLE_1:1
.=
((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . c
by A11, FUNCT_1:49
;
hence
f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !))
by A12, A13;
verum end; case A15:
x = x0
;
ex s being set st
( 0 < s & s < 1 & ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x )set s = 1
/ 2;
take s = 1
/ 2;
( 0 < s & s < 1 & ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x )thus
(
0 < s &
s < 1 )
;
((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . xset c =
x0 + (s * (x - x0));
thus ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) =
(f . x) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x) |^ (n + 1))) / ((n + 1) !))
by A4, A15, Th32
.=
(f . x) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((0 |^ n) * 0)) / ((n + 1) !))
by NEWTON:6
.=
f . x
;
verum end; case A16:
x > x0
;
ex s being set st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )set t =
x - x0;
A17:
f is_differentiable_on n,
].(x0 - r),(x0 + r).[
by A3, Th23, NAT_1:11;
|.(x0 - x0).| = 0
by ABSVALUE:2;
then
x0 in ].(x0 - r),(x0 + r).[
by A2, RCOMP_1:1;
then A18:
[.x0,x.] c= ].(x0 - r),(x0 + r).[
by A4, XXREAL_2:def 12;
(diff (f,].(x0 - r),(x0 + r).[)) . n is_differentiable_on ].(x0 - r),(x0 + r).[
by A3;
then
((diff (f,].(x0 - r),(x0 + r).[)) . n) | ].(x0 - r),(x0 + r).[ is
continuous
by FDIFF_1:25;
then A19:
((diff (f,].(x0 - r),(x0 + r).[)) . n) | [.x0,x.] is
continuous
by A18, FCONT_1:16;
A20:
].x0,x.[ c= [.x0,x.]
by XXREAL_1:25;
then
f is_differentiable_on n + 1,
].x0,x.[
by A3, A18, Th31, XBOOLE_1:1;
then consider c being
Real such that A21:
c in ].x0,x.[
and A22:
f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].x0,x.[)) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !))
by A1, A16, A18, A17, A19, Th27;
take s =
(c - x0) / (x - x0);
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )A23:
x - x0 > 0
by A16, XREAL_1:50;
then A24:
x0 + (s * (x - x0)) =
x0 + (c - x0)
by XCMPLX_1:87
.=
c
;
c in { p where p is Real : ( x0 < p & p < x0 + (x - x0) ) }
by A21, RCOMP_1:def 2;
then A25:
ex
g being
Real st
(
g = c &
x0 < g &
g < x0 + (x - x0) )
;
then
0 < c - x0
by XREAL_1:50;
then
0 / (x - x0) < (c - x0) / (x - x0)
by A23, XREAL_1:74;
hence
0 < s
;
( s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
c - x0 < x - x0
by A25, XREAL_1:19;
then
(c - x0) / (x - x0) < (x - x0) / (x - x0)
by A23, XREAL_1:74;
hence
s < 1
by A23, XCMPLX_1:60;
f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !))((diff (f,].x0,x.[)) . (n + 1)) . c =
(((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) | ].x0,x.[) . c
by A3, A18, A20, Th30, XBOOLE_1:1
.=
((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . c
by A21, FUNCT_1:49
;
hence
f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !))
by A22, A24;
verum end;
hence
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
; verum