let p be Real; :: 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)) )
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)) ) )
A1: ( p is Real & exp_R is_differentiable_in p ) by SIN_COS:65;
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 * f is_differentiable_in p by Lm13;
then A4: diff ((exp_R + (exp_R * f)),p) = (diff (exp_R,p)) + (diff ((exp_R * f),p)) by A1, FDIFF_1:13
.= (exp_R . p) + (diff ((exp_R * f),p)) by SIN_COS:65
.= (exp_R . p) + ((- 1) * (exp_R . (f . p))) by A2, Lm13
.= (exp_R . p) + ((- 1) * (exp_R . ((- 1) * p))) by A2, Lm10
.= (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:14
.= (exp_R . p) - (diff ((exp_R * f),p)) by SIN_COS:65
.= (exp_R . p) - ((- 1) * (exp_R . (f . p))) by A2, Lm13
.= (exp_R . p) - ((- 1) * (exp_R . ((- 1) * p))) by A2, Lm10
.= (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:13, FDIFF_1:14; :: thesis: verum