let x be Real; :: thesis: ( sin . x <> 0 implies ( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) ) )
assume A1: sin . x <> 0 ; :: thesis: ( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) )
A2: ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64;
then diff ((cos / sin),x) = (((diff (cos,x)) * (sin . x)) - ((diff (sin,x)) * (cos . x))) / ((sin . x) ^2) by A1, FDIFF_2:14
.= (((- (sin . x)) * (sin . x)) - ((diff (sin,x)) * (cos . x))) / ((sin . x) ^2) by SIN_COS:63
.= ((- ((sin . x) * (sin . x))) - ((cos . x) * (cos . x))) / ((sin . x) ^2) by SIN_COS:64
.= (- (((cos . x) ^2) + ((sin . x) * (sin . x)))) / ((sin . x) ^2)
.= - ((((cos . x) ^2) + ((sin . x) ^2)) / ((sin . x) ^2)) by XCMPLX_1:187
.= - (1 / ((sin . x) ^2)) by SIN_COS:28 ;
hence ( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) ) by A2, A1, FDIFF_2:14; :: thesis: verum