let x be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds
( arctan * f is_differentiable_in x & diff (arctan * f),x = (diff f,x) / (1 + ((f . x) ^2 )) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_in x & f . x > - 1 & f . x < 1 implies ( arctan * f is_differentiable_in x & diff (arctan * f),x = (diff f,x) / (1 + ((f . x) ^2 )) ) )
assume that
A1: f is_differentiable_in x and
A2: f . x > - 1 and
A3: f . x < 1 ; :: thesis: ( arctan * f is_differentiable_in x & diff (arctan * f),x = (diff f,x) / (1 + ((f . x) ^2 )) )
f . x in ].(- 1),1.[ by A2, A3, XXREAL_1:4;
then A4: arctan is_differentiable_in f . x by Th73, FDIFF_1:16;
then diff (arctan * f),x = (diff arctan ,(f . x)) * (diff f,x) by A1, FDIFF_2:13
.= (diff f,x) * (1 / (1 + ((f . x) ^2 ))) by A2, A3, Th75
.= (diff f,x) / (1 + ((f . x) ^2 )) ;
hence ( arctan * f is_differentiable_in x & diff (arctan * f),x = (diff f,x) / (1 + ((f . x) ^2 )) ) by A1, A4, FDIFF_2:13; :: thesis: verum