:: by Yasunari Shidama

::

:: Received February 24, 2004

:: Copyright (c) 2004-2012 Association of Mizar Users

begin

definition

let q be Integer;

ex b_{1} being Function of REAL,REAL st

for x being real number holds b_{1} . x = x #Z q

for b_{1}, b_{2} being Function of REAL,REAL st ( for x being real number holds b_{1} . x = x #Z q ) & ( for x being real number holds b_{2} . x = x #Z q ) holds

b_{1} = b_{2}

end;
func #Z q -> Function of REAL,REAL means :Def1: :: TAYLOR_1:def 1

for x being real number holds it . x = x #Z q;

existence for x being real number holds it . x = x #Z q;

ex b

for x being real number holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines #Z TAYLOR_1:def 1 :

for q being Integer

for b_{2} being Function of REAL,REAL holds

( b_{2} = #Z q iff for x being real number holds b_{2} . x = x #Z q );

for q being Integer

for b

( b

theorem Th2: :: TAYLOR_1:2

for n being Nat

for x being real number holds

( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )

for x being real number holds

( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )

proof end;

theorem :: TAYLOR_1:3

for n being Nat

for x0 being real number

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds

( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )

for x0 being real number

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds

( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )

proof end;

Lm1: for n being Nat

for x being real number holds (exp_R x) #R n = exp_R (n * x)

proof end;

Lm2: for i being Integer

for x being real number holds (exp_R x) #R i = exp_R (i * x)

proof end;

Lm3: for x being real number

for q being Rational holds (exp_R x) #R q = exp_R (q * x)

proof end;

theorem Th9: :: TAYLOR_1:9

for x being real number holds

( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )

( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )

proof end;

theorem :: TAYLOR_1:10

for x being real number holds

( (exp_R . 1) #R x = exp_R . x & (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x )

( (exp_R . 1) #R x = exp_R . x & (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x )

proof end;

then Lm4: number_e > 1

by XXREAL_0:2;

theorem Th16: :: TAYLOR_1:16

( exp_R is one-to-one & exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL & ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )

proof end;

theorem Th17: :: TAYLOR_1:17

( exp_R " is_differentiable_on dom (exp_R ") & ( for x being real number st x in dom (exp_R ") holds

diff ((exp_R "),x) = 1 / x ) )

diff ((exp_R "),x) = 1 / x ) )

proof end;

definition

let a be real number ;

ex b_{1} being PartFunc of REAL,REAL st

( dom b_{1} = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b_{1} . d = log (a,d) ) )

for b_{1}, b_{2} being PartFunc of REAL,REAL st dom b_{1} = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b_{1} . d = log (a,d) ) & dom b_{2} = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b_{2} . d = log (a,d) ) holds

b_{1} = b_{2}

end;
func log_ a -> PartFunc of REAL,REAL means :Def2: :: TAYLOR_1:def 2

( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = log (a,d) ) );

existence ( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = log (a,d) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines log_ TAYLOR_1:def 2 :

for a being real number

for b_{2} being PartFunc of REAL,REAL holds

( b_{2} = log_ a iff ( dom b_{2} = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b_{2} . d = log (a,d) ) ) );

for a being real number

for b

( b

theorem Th18: :: TAYLOR_1:18

( ln = exp_R " & ln is one-to-one & dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds

ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) )

ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) )

proof end;

theorem :: TAYLOR_1:19

for x0 being real number

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds

( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) )

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds

( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) )

proof end;

theorem :: TAYLOR_1:20

for x0 being real number

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds

( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds

( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )

proof end;

definition

let p be real number ;

ex b_{1} being PartFunc of REAL,REAL st

( dom b_{1} = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b_{1} . d = d #R p ) )

for b_{1}, b_{2} being PartFunc of REAL,REAL st dom b_{1} = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b_{1} . d = d #R p ) & dom b_{2} = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b_{2} . d = d #R p ) holds

b_{1} = b_{2}

end;
func #R p -> PartFunc of REAL,REAL means :Def4: :: TAYLOR_1:def 4

( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = d #R p ) );

existence ( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = d #R p ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines #R TAYLOR_1:def 4 :

for p being real number

for b_{2} being PartFunc of REAL,REAL holds

( b_{2} = #R p iff ( dom b_{2} = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b_{2} . d = d #R p ) ) );

for p being real number

for b

( b

theorem Th21: :: TAYLOR_1:21

for x, p being real number st x > 0 holds

( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) )

( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) )

proof end;

theorem :: TAYLOR_1:22

for x0, p being real number

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds

( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) )

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds

( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) )

proof end;

begin

definition

let f be PartFunc of REAL,REAL;

let Z be Subset of REAL;

ex b_{1} being Functional_Sequence of REAL,REAL st

( b_{1} . 0 = f | Z & ( for i being Nat holds b_{1} . (i + 1) = (b_{1} . i) `| Z ) )

for b_{1}, b_{2} being Functional_Sequence of REAL,REAL st b_{1} . 0 = f | Z & ( for i being Nat holds b_{1} . (i + 1) = (b_{1} . i) `| Z ) & b_{2} . 0 = f | Z & ( for i being Nat holds b_{2} . (i + 1) = (b_{2} . i) `| Z ) holds

b_{1} = b_{2}

end;
let Z be Subset of REAL;

func diff (f,Z) -> Functional_Sequence of REAL,REAL means :Def5: :: TAYLOR_1:def 5

( it . 0 = f | Z & ( for i being Nat holds it . (i + 1) = (it . i) `| Z ) );

existence ( it . 0 = f | Z & ( for i being Nat holds it . (i + 1) = (it . i) `| Z ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines diff TAYLOR_1:def 5 :

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for b_{3} being Functional_Sequence of REAL,REAL holds

( b_{3} = diff (f,Z) iff ( b_{3} . 0 = f | Z & ( for i being Nat holds b_{3} . (i + 1) = (b_{3} . i) `| Z ) ) );

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for b

( b

definition

let f be PartFunc of REAL,REAL;

let n be Nat;

let Z be Subset of REAL;

end;
let n be Nat;

let Z be Subset of REAL;

pred f is_differentiable_on n,Z means :Def6: :: TAYLOR_1:def 6

for i being Element of NAT st i <= n - 1 holds

(diff (f,Z)) . i is_differentiable_on Z;

for i being Element of NAT st i <= n - 1 holds

(diff (f,Z)) . i is_differentiable_on Z;

:: deftheorem Def6 defines is_differentiable_on TAYLOR_1:def 6 :

for f being PartFunc of REAL,REAL

for n being Nat

for Z being Subset of REAL holds

( f is_differentiable_on n,Z iff for i being Element of NAT st i <= n - 1 holds

(diff (f,Z)) . i is_differentiable_on Z );

for f being PartFunc of REAL,REAL

for n being Nat

for Z being Subset of REAL holds

( f is_differentiable_on n,Z iff for i being Element of NAT st i <= n - 1 holds

(diff (f,Z)) . i is_differentiable_on Z );

theorem Th23: :: TAYLOR_1:23

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for n being Nat st f is_differentiable_on n,Z holds

for m being Nat st m <= n holds

f is_differentiable_on m,Z

for Z being Subset of REAL

for n being Nat st f is_differentiable_on n,Z holds

for m being Nat st m <= n holds

f is_differentiable_on m,Z

proof end;

definition

let f be PartFunc of REAL,REAL;

let Z be Subset of REAL;

let a, b be real number ;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) & ( for n being Nat holds b_{2} . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) holds

b_{1} = b_{2}

end;
let Z be Subset of REAL;

let a, b be real number ;

func Taylor (f,Z,a,b) -> Real_Sequence means :Def7: :: TAYLOR_1:def 7

for n being Nat holds it . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !);

existence for n being Nat holds it . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines Taylor TAYLOR_1:def 7 :

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for a, b being real number

for b_{5} being Real_Sequence holds

( b_{5} = Taylor (f,Z,a,b) iff for n being Nat holds b_{5} . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) );

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for a, b being real number

for b

( b

Lm5: for b being Real ex g being PartFunc of REAL,REAL st

( dom g = [#] REAL & ( for x being Real holds

( g . x = b - x & ( for x being Real holds

( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) )

proof end;

Lm6: for n being Element of NAT

for l, b being Real ex g being PartFunc of REAL,REAL st

( dom g = [#] REAL & ( for x being Real holds

( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds

( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) )

proof end;

Lm7: for n being Element of NAT

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for b being Real ex 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) ) )

proof end;

theorem Th24: :: TAYLOR_1:24

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

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 holds

((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n

for Z being Subset of REAL

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 holds

((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n

proof end;

Lm8: for f being PartFunc of REAL,REAL

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 !)) ) )

proof end;

Lm9: for n being Element of 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 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) ) & 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 !)) ) )

proof end;

theorem Th25: :: TAYLOR_1:25

for n being Element of 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

for l being Real

for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds

( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds

diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) )

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

for l being Real

for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds

( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds

diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) )

proof end;

theorem Th26: :: TAYLOR_1:26

for n being Element of NAT

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for b, l being Real ex g being Function of REAL,REAL st

for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for b, l being Real ex g being Function of REAL,REAL st

for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))

proof end;

theorem Th27: :: TAYLOR_1:27

for n being Element of 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 . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) )

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 . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) )

proof end;

Lm10: for f being PartFunc of REAL,REAL

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 . 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 !)) ) )

proof end;

Lm11: for n being Element of 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 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) ) & 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 !)) ) )

proof end;

theorem Th28: :: TAYLOR_1:28

for n being Element of 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

for l being Real

for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds

( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds

diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )

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

for l being Real

for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds

( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds

diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )

proof end;

theorem Th29: :: TAYLOR_1:29

for n being Element of 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) !)) )

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) !)) )

proof end;

theorem Th30: :: TAYLOR_1:30

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for Z1 being open Subset of REAL st Z1 c= Z holds

for n being Element of NAT st f is_differentiable_on n,Z holds

((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n

for Z being Subset of REAL

for Z1 being open Subset of REAL st Z1 c= Z holds

for n being Element of NAT st f is_differentiable_on n,Z holds

((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n

proof end;

theorem Th31: :: TAYLOR_1:31

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for Z1 being open Subset of REAL st Z1 c= Z holds

for n being Nat st f is_differentiable_on n + 1,Z holds

f is_differentiable_on n + 1,Z1

for Z being Subset of REAL

for Z1 being open Subset of REAL st Z1 c= Z holds

for n being Nat st f is_differentiable_on n + 1,Z holds

f is_differentiable_on n + 1,Z1

proof end;

theorem Th32: :: TAYLOR_1:32

for f being PartFunc of REAL,REAL

for Z being Subset of REAL

for x being Real st x in Z holds

for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

for Z being Subset of REAL

for x being Real st x in Z holds

for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

proof end;

:: Taylor's Theorem

theorem :: TAYLOR_1:33

for n being Element of 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) !)) )

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) !)) )

proof end;