let n be Nat; :: thesis: for a, b being real number st a < b holds
ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
let a, b be real number ; :: thesis: ( a < b implies ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) )
assume A1: a < b ; :: thesis: ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
set f = exp_R ;
set Z = [#] REAL;
A2: n in NAT by ORDINAL1:def 12;
then A3: exp_R is_differentiable_on n, [#] REAL by TAYLOR_2:10;
(diff (exp_R,([#] REAL))) . n = exp_R | ([#] REAL) by A2, TAYLOR_2:6;
then A4: ((diff (exp_R,([#] REAL))) . n) | [.a,b.] is continuous ;
A5: exp_R is_differentiable_on n + 1,].a,b.[ by TAYLOR_2:10;
( a in REAL & b in REAL ) by XREAL_0:def 1;
then consider c being Real such that
A6: c in ].a,b.[ and
A7: exp_R . a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((((diff (exp_R,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) by A1, A3, A4, A5, A2, SIN_COS:47, TAYLOR_1:29;
take c ; :: thesis: ( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
thus ( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) by A7, A6, TAYLOR_2:7; :: thesis: verum