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