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
( arccot * f is_differentiable_in x & diff ((arccot * 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 ( arccot * f is_differentiable_in x & diff ((arccot * 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: ( arccot * f is_differentiable_in x & diff ((arccot * f),x) = - ((diff (f,x)) / (1 + ((f . x) ^2))) )
f . x in ].(- 1),1.[ by A2, A3, XXREAL_1:4;
then A4: arccot is_differentiable_in f . x by Th74, FDIFF_1:9;
then diff ((arccot * f),x) = (diff (arccot,(f . x))) * (diff (f,x)) by A1, FDIFF_2:13
.= (diff (f,x)) * (- (1 / (1 + ((f . x) ^2)))) by A2, A3, Th76
.= - ((diff (f,x)) / (1 + ((f . x) ^2))) ;
hence ( arccot * f is_differentiable_in x & diff ((arccot * f),x) = - ((diff (f,x)) / (1 + ((f . x) ^2))) ) by A1, A4, FDIFF_2:13; :: thesis: verum