let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: for x0 being positive Real st len f > 0 holds
ex s being Real st
( 0 < s & s < 1 & (('F' f) . x0) - ((exp_R . x0) * (('F' f) . 0)) = - ((x0 * (exp_R . (x0 * (1 - s)))) * ((Eval (~ (^ f))) . (s * x0))) )
let x0 be positive Real; :: thesis: ( len f > 0 implies ex s being Real st
( 0 < s & s < 1 & (('F' f) . x0) - ((exp_R . x0) * (('F' f) . 0)) = - ((x0 * (exp_R . (x0 * (1 - s)))) * ((Eval (~ (^ f))) . (s * x0))) ) )
assume A1: len f > 0 ; :: thesis: ex s being Real st
( 0 < s & s < 1 & (('F' f) . x0) - ((exp_R . x0) * (('F' f) . 0)) = - ((x0 * (exp_R . (x0 * (1 - s)))) * ((Eval (~ (^ f))) . (s * x0))) )
set PHI = exp_R1 (#) ('F' f);
consider s being Real such that
A2: ( 0 < s & s < 1 ) and
A3: (exp_R1 (#) ('F' f)) . x0 = ((exp_R1 (#) ('F' f)) . 0) + (x0 * (diff ((exp_R1 (#) ('F' f)),(s * x0)))) by Lm33;
A4: (exp_R1 (#) ('F' f)) . x0 = (exp_R1 . x0) * (('F' f) . x0) by VALUED_1:5;
A5: (exp_R1 (#) ('F' f)) . 0 = (exp_R1 . 0) * (('F' f) . 0) by VALUED_1:5
.= ((exp_R . 0) ") * (('F' f) . 0) by RFUNCT_1:59
.= (1 ") * (('F' f) . 0) by SIN_COS:51, SIN_COS:def 23
.= ('F' f) . 0 ;
reconsider PHi = exp_R1 (#) ('F' f) as differentiable Function of REAL,REAL ;
A6: diff ((exp_R1 (#) ('F' f)),(s * x0)) = (PHi `|) . (s * x0) by POLYDIFF:10
.= (- (exp_R1 (#) (Eval (~ (^ f))))) . (s * x0) by A1, Lm36
.= - ((exp_R1 (#) (Eval (~ (^ f)))) . (s * x0)) by VALUED_1:8
.= - ((exp_R1 . (s * x0)) * ((Eval (~ (^ f))) . (s * x0))) by VALUED_1:5 ;
A7: x0 in dom (exp_R ^) by Lm23A, XREAL_0:def 1;
A8: exp_R . x0 <> 0 by SIN_COS:54;
A9: x0 * s in dom (exp_R ^) by Lm23A, XREAL_0:def 1;
reconsider x1 = x0 * s as Real ;
reconsider r = exp_R . x0 as Real ;
A10: exp_R1 . (s * x0) = 1 / (exp_R . x1) by A9, RFUNCT_1:59
.= 1 / (exp_R x1) by SIN_COS:def 23
.= exp_R (- x1) by TAYLOR_1:4
.= exp_R . (- x1) by SIN_COS:def 23 ;
(('F' f) . x0) - ((exp_R . x0) * (('F' f) . 0)) = (1 * (('F' f) . x0)) - ((exp_R . x0) * (('F' f) . 0))
.= ((r * (r ")) * (('F' f) . x0)) - ((exp_R . x0) * (('F' f) . 0)) by A8, XCMPLX_0:def 7
.= (((exp_R . x0) * (exp_R1 . x0)) * (('F' f) . x0)) - ((exp_R . x0) * (('F' f) . 0)) by A7, RFUNCT_1:59
.= (exp_R . x0) * (((exp_R1 (#) ('F' f)) . x0) - ((exp_R1 (#) ('F' f)) . 0)) by A5, A4
.= - ((x0 * ((exp_R . x0) * (exp_R . (- (s * x0))))) * ((Eval (~ (^ f))) . (s * x0))) by A10, A6, A3
.= - ((x0 * (exp_R . (x0 + (- (s * x0))))) * ((Eval (~ (^ f))) . (s * x0))) by SIN_COS2:12
.= - ((x0 * (exp_R . (x0 * (1 - s)))) * ((Eval (~ (^ f))) . (s * x0))) ;
hence ex s being Real st
( 0 < s & s < 1 & (('F' f) . x0) - ((exp_R . x0) * (('F' f) . 0)) = - ((x0 * (exp_R . (x0 * (1 - s)))) * ((Eval (~ (^ f))) . (s * x0))) ) by A2; :: thesis: verum