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