let n be Nat; 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; ( 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
; 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
; ( 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; verum