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 13;
then A3: exp_R is_differentiable_on n, [#] REAL by TAYLOR_2:10;
(diff exp_R ,([#] REAL )) . n = exp_R | ([#] REAL ) by TAYLOR_2:6, A2;
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, SIN_COS:51, A3, A4, A5, TAYLOR_1:29, A2;
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