let n be Nat; :: thesis: for a, b being Real st a < b holds
ex c being Real 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; :: thesis: ( a < b implies ex c being Real 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 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;
n in NAT by ORDINAL1:def 12;
then A2: exp_R is_differentiable_on n, [#] REAL by TAYLOR_2:10;
(diff (exp_R,([#] REAL))) . n = exp_R | ([#] REAL) by TAYLOR_2:6;
then A3: ((diff (exp_R,([#] REAL))) . n) | [.a,b.] is continuous ;
A4: exp_R is_differentiable_on n + 1,].a,b.[ by TAYLOR_2:10;
consider c being Real such that
A5: c in ].a,b.[ and
A6: 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, A2, A3, A4, 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 A6, A5, TAYLOR_2:7; :: thesis: verum