let x0, x1 be Real; :: thesis: [!(() (#) cos),x0,x1!] = - (((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1))
set y = 3 * x0;
set z = 3 * x1;
[!(() (#) cos),x0,x1!] = (((() . x0) * (cos . x0)) - ((() (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((sin . x0) * (sin . x0)) * (cos . x0)) - ((() (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((sin . x0) * (sin . x0)) * (cos . x0)) - ((() . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= ((((sin x0) * (sin x0)) * (cos x0)) - (((sin x1) * (sin x1)) * (cos x1))) / (x0 - x1) by VALUED_1:5
.= (((1 / 4) * ((((- (cos ((x0 + x0) - x0))) + (cos ((x0 + x0) - x0))) + (cos ((x0 + x0) - x0))) - (cos ((x0 + x0) + x0)))) - (((sin x1) * (sin x1)) * (cos x1))) / (x0 - x1) by SIN_COS4:34
.= (((1 / 4) * ((cos x0) - (cos (3 * x0)))) - ((1 / 4) * ((((- (cos ((x1 + x1) - x1))) + (cos ((x1 + x1) - x1))) + (cos ((x1 + x1) - x1))) - (cos ((x1 + x1) + x1))))) / (x0 - x1) by SIN_COS4:34
.= (((1 / 4) * ((cos x0) - (cos x1))) + ((1 / 4) * ((cos (3 * x1)) - (cos (3 * x0))))) / (x0 - x1)
.= (((1 / 4) * (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) + ((1 / 4) * ((cos (3 * x1)) - (cos (3 * x0))))) / (x0 - x1) by SIN_COS4:18
.= (((1 / 4) * (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) + ((1 / 4) * (- (2 * ((sin (((3 * x1) + (3 * x0)) / 2)) * (sin (((3 * x1) - (3 * x0)) / 2))))))) / (x0 - x1) by SIN_COS4:18
.= (- ((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) / (x0 - x1) ;
hence [!(() (#) cos),x0,x1!] = - (((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1)) by XCMPLX_1:187; :: thesis: verum