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
( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_in x & f . x > - 1 & f . x < 1 implies ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) ) )
assume that
A1: f is_differentiable_in x and
A2: ( f . x > - 1 & f . x < 1 ) ; :: thesis: ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) )
f . x in ].(- 1),1.[ by A2;
then A3: arccos is_differentiable_in f . x by FDIFF_1:9, SIN_COS6:106;
then diff ((arccos * f),x) = (diff (arccos,(f . x))) * (diff (f,x)) by A1, FDIFF_2:13
.= (- (1 / (sqrt (1 - ((f . x) ^2))))) * (diff (f,x)) by A2, SIN_COS6:106
.= - ((diff (f,x)) * (1 / (sqrt (1 - ((f . x) ^2)))))
.= - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) by XCMPLX_1:99 ;
hence ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) ) by A1, A3, FDIFF_2:13; :: thesis: verum