let h, x be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) & sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = ((((16 * (cos x)) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin x)) / (((cos (2 * x)) - (cos h)) ^2)
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = 1 / ((sin x) ^2) ) & sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 implies (cD (f,h)) . x = ((((16 * (cos x)) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin x)) / (((cos (2 * x)) - (cos h)) ^2) )
assume that
A1: for x being Real holds f . x = 1 / ((sin x) ^2) and
A2: ( sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 ) ; :: thesis: (cD (f,h)) . x = ((((16 * (cos x)) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin x)) / (((cos (2 * x)) - (cos h)) ^2)
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (1 / ((sin (x + (h / 2))) ^2)) - (f . (x - (h / 2))) by A1
.= (1 / ((sin (x + (h / 2))) ^2)) - (1 / ((sin (x - (h / 2))) ^2)) by A1
.= ((1 * ((sin (x - (h / 2))) ^2)) - (1 * ((sin (x + (h / 2))) ^2))) / (((sin (x + (h / 2))) ^2) * ((sin (x - (h / 2))) ^2)) by A2, XCMPLX_1:130
.= (((sin (x - (h / 2))) ^2) - ((sin (x + (h / 2))) ^2)) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)
.= (((sin (x - (h / 2))) ^2) - ((sin (x + (h / 2))) ^2)) / ((- ((1 / 2) * ((cos ((x + (h / 2)) + (x - (h / 2)))) - (cos ((x + (h / 2)) - (x - (h / 2))))))) ^2) by SIN_COS4:29
.= (((sin (x - (h / 2))) ^2) - ((sin (x + (h / 2))) ^2)) / ((1 / 4) * (((cos (2 * x)) - (cos h)) ^2))
.= ((((sin (x - (h / 2))) ^2) - ((sin (x + (h / 2))) ^2)) / (1 / 4)) / (((cos (2 * x)) - (cos h)) ^2) by XCMPLX_1:78
.= 4 * ((((sin (x - (h / 2))) - (sin (x + (h / 2)))) * ((sin (x - (h / 2))) + (sin (x + (h / 2))))) / (((cos (2 * x)) - (cos h)) ^2))
.= 4 * (((2 * ((cos (((x - (h / 2)) + (x + (h / 2))) / 2)) * (sin (((x - (h / 2)) - (x + (h / 2))) / 2)))) * ((sin (x - (h / 2))) + (sin (x + (h / 2))))) / (((cos (2 * x)) - (cos h)) ^2)) by SIN_COS4:16
.= 4 * (((2 * ((cos ((2 * x) / 2)) * (sin ((- h) / 2)))) * (2 * ((cos ((- h) / 2)) * (sin ((2 * x) / 2))))) / (((cos (2 * x)) - (cos h)) ^2)) by SIN_COS4:15
.= ((((16 * (cos x)) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin x)) / (((cos (2 * x)) - (cos h)) ^2) ;
hence (cD (f,h)) . x = ((((16 * (cos x)) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin x)) / (((cos (2 * x)) - (cos h)) ^2) ; :: thesis: verum