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