let th1, th2 be Real; :: thesis: ( cos th1 <> 0 & cos th2 <> 0 implies (sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2)) )
assume that
A1: cos th1 <> 0 and
A2: cos th2 <> 0 ; :: thesis: (sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2))
(sin (th1 + th2)) / (sin (th1 - th2)) = (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / (sin (th1 - th2)) by SIN_COS:75
.= (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / (((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) by SIN_COS:82
.= ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) by A1, A2, XCMPLX_1:55
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((sin th1) * (cos th2)) + (- ((cos th1) * (sin th2)))) / ((cos th1) * (cos th2))) by XCMPLX_1:62
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + ((- ((cos th1) * (sin th2))) / ((cos th1) * (cos th2)))) by XCMPLX_1:62
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + ((- ((cos th1) * (sin th2))) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((sin th2) / (cos th2)))) / ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + ((- ((cos th1) * (sin th2))) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((sin th2) / (cos th2)))) / ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) * (- (sin th2))) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((sin th2) / (cos th2)))) / ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((- (sin th2)) / (cos th2)))) by XCMPLX_1:76
.= (((sin th1) / (cos th1)) + (((cos th1) / (cos th1)) * ((sin th2) / (cos th2)))) / ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((- (sin th2)) / (cos th2)))) by A2, XCMPLX_1:88
.= (((sin th1) / (cos th1)) + ((sin th2) / (cos th2))) / ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((- (sin th2)) / (cos th2)))) by A1, XCMPLX_1:88
.= (((sin th1) / (cos th1)) + ((sin th2) / (cos th2))) / (((sin th1) / (cos th1)) + (((cos th1) / (cos th1)) * ((- (sin th2)) / (cos th2)))) by A2, XCMPLX_1:88
.= (((sin th1) / (cos th1)) + ((sin th2) / (cos th2))) / (((sin th1) / (cos th1)) + ((- (sin th2)) / (cos th2))) by A1, XCMPLX_1:88
.= ((tan th1) + (tan th2)) / ((tan th1) + (- ((sin th2) / (cos th2)))) by XCMPLX_1:187
.= ((tan th1) + (tan th2)) / ((tan th1) - (tan th2)) ;
hence (sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2)) ; :: thesis: verum