let p be real number ; :: thesis: for f being PartFunc of REAL ,REAL st f = compreal holds
( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff (exp_R - (exp_R * f)),p = (exp_R . p) + (exp_R . (- p)) & diff (exp_R + (exp_R * f)),p = (exp_R . p) - (exp_R . (- p)) )
A1: p is Real by XREAL_0:def 1;
let f be PartFunc of REAL ,REAL ; :: thesis: ( f = compreal implies ( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff (exp_R - (exp_R * f)),p = (exp_R . p) + (exp_R . (- p)) & diff (exp_R + (exp_R * f)),p = (exp_R . p) - (exp_R . (- p)) ) )
assume A2: f = compreal ; :: thesis: ( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff (exp_R - (exp_R * f)),p = (exp_R . p) + (exp_R . (- p)) & diff (exp_R + (exp_R * f)),p = (exp_R . p) - (exp_R . (- p)) )
then A3: ( exp_R is_differentiable_in p & exp_R * f is_differentiable_in p ) by Lm14, SIN_COS:70;
then A4: diff (exp_R - (exp_R * f)),p = (diff exp_R ,p) - (diff (exp_R * f),p) by A1, FDIFF_1:22
.= (exp_R . p) - (diff (exp_R * f),p) by SIN_COS:70
.= (exp_R . p) - ((- 1) * (exp_R . (f . p))) by A2, Lm14
.= (exp_R . p) - ((- 1) * (exp_R . ((- 1) * p))) by A2, Lm11
.= (exp_R . p) + (exp_R . (- p)) ;
diff (exp_R + (exp_R * f)),p = (diff exp_R ,p) + (diff (exp_R * f),p) by A1, A3, FDIFF_1:21
.= (exp_R . p) + (diff (exp_R * f),p) by SIN_COS:70
.= (exp_R . p) + ((- 1) * (exp_R . (f . p))) by A2, Lm14
.= (exp_R . p) + ((- 1) * (exp_R . ((- 1) * p))) by A2, Lm11
.= (exp_R . p) - (exp_R . (- p)) ;
hence ( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff (exp_R - (exp_R * f)),p = (exp_R . p) + (exp_R . (- p)) & diff (exp_R + (exp_R * f)),p = (exp_R . p) - (exp_R . (- p)) ) by A1, A3, A4, FDIFF_1:21, FDIFF_1:22; :: thesis: verum