let x, h 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
(fD 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 (fD 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: (fD 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 )
(fD f,h) . x = (f . (x + h)) - (f . x) by DIFF_1:3
.= (1 / ((cos (x + h)) ^2 )) - (f . x) by A1
.= (1 / ((cos (x + h)) ^2 )) - (1 / ((cos x) ^2 )) by A1
.= ((1 * ((cos x) ^2 )) - (1 * ((cos (x + h)) ^2 ))) / (((cos (x + h)) ^2 ) * ((cos x) ^2 )) by A2, XCMPLX_1:131
.= (((cos x) ^2 ) - ((cos (x + h)) ^2 )) / (((cos (x + h)) * (cos x)) ^2 )
.= (((cos x) ^2 ) - ((cos (x + h)) ^2 )) / (((1 / 2) * ((cos ((x + h) + x)) + (cos ((x + h) - x)))) ^2 ) by SIN_COS4:36
.= (((cos x) ^2 ) - ((cos (x + h)) ^2 )) / ((1 / 4) * (((cos ((2 * x) + h)) + (cos h)) ^2 ))
.= ((((cos x) ^2 ) - ((cos (x + h)) ^2 )) / (1 / 4)) / (((cos ((2 * x) + h)) + (cos h)) ^2 ) by XCMPLX_1:79
.= 4 * ((((cos x) - (cos (x + h))) * ((cos x) + (cos (x + h)))) / (((cos ((2 * x) + h)) + (cos h)) ^2 ))
.= 4 * (((- (2 * ((sin ((x + (x + h)) / 2)) * (sin ((x - (x + h)) / 2))))) * ((cos x) + (cos (x + h)))) / (((cos ((2 * x) + h)) + (cos h)) ^2 )) by SIN_COS4:22
.= 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:21
.= (((((- 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 (fD 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