let th1, th2 be Real; :: thesis: ( cos ((th1 + th2) / 2) <> 0 implies ((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 - th2) / 2) )
assume A1: cos ((th1 + th2) / 2) <> 0 ; :: thesis: ((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 - th2) / 2)
((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / ((cos th1) + (cos th2)) by Th16
.= (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) by Th17
.= (2 / 2) * (((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))) / ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) by XCMPLX_1:76
.= ((cos ((th1 + th2) / 2)) / (cos ((th1 + th2) / 2))) * ((sin ((th1 - th2) / 2)) / (cos ((th1 - th2) / 2))) by XCMPLX_1:76
.= tan ((th1 - th2) / 2) by A1, XCMPLX_1:88 ;
hence ((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 - th2) / 2) ; :: thesis: verum