let x0, x1 be Real; :: thesis: ( x0 in dom cosec & x1 in dom cosec implies [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) )
assume that
A1: x0 in dom cosec and
A2: x1 in dom cosec ; :: thesis: [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1))
A3: cosec . x1 = (sin . x1) " by
.= cosec x1 by XCMPLX_1:215 ;
cosec . x0 = (sin . x0) " by
.= cosec x0 by XCMPLX_1:215 ;
then [!cosec,x0,x1!] = (((1 * (sin x1)) / ((sin x0) * (sin x1))) - (1 / (sin x1))) / (x0 - x1) by
.= (((1 * (sin x1)) / ((sin x0) * (sin x1))) - ((1 * (sin x0)) / ((sin x1) * (sin x0)))) / (x0 - x1) by
.= (((sin x1) - (sin x0)) / ((sin x1) * (sin x0))) / (x0 - x1) by XCMPLX_1:120
.= ((sin x1) - (sin x0)) / (((sin x1) * (sin x0)) * (x0 - x1)) by XCMPLX_1:78
.= (2 * ((cos ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((sin x1) * (sin x0)) * (x0 - x1)) by SIN_COS4:16 ;
hence [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) ; :: thesis: verum