let x, h be Real; :: thesis: for f being Function of REAL ,REAL st ( for x being Real holds f . x = (tan (#) tan ) . x ) & x in dom tan & x + h in dom tan holds
(fD f,h) . x = - (((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((cos (x + h)) * (cos x)) ^2 ))
let f be Function of REAL ,REAL ; :: thesis: ( ( for x being Real holds f . x = (tan (#) tan ) . x ) & x in dom tan & x + h in dom tan implies (fD f,h) . x = - (((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((cos (x + h)) * (cos x)) ^2 )) )
assume that
A1: for x being Real holds f . x = (tan (#) tan ) . x and
A2: ( x in dom tan & x + h in dom tan ) ; :: thesis: (fD f,h) . x = - (((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((cos (x + h)) * (cos x)) ^2 ))
A3: ( cos x <> 0 & cos (x + h) <> 0 ) by A2, FDIFF_8:1;
(fD f,h) . x = (f . (x + h)) - (f . x) by DIFF_1:3
.= ((tan (#) tan ) . (x + h)) - (f . x) by A1
.= ((tan (#) tan ) . (x + h)) - ((tan (#) tan ) . x) by A1
.= ((tan . (x + h)) * (tan . (x + h))) - ((tan (#) tan ) . x) by VALUED_1:5
.= ((tan . (x + h)) * (tan . (x + h))) - ((tan . x) * (tan . x)) by VALUED_1:5
.= (((sin . (x + h)) * ((cos . (x + h)) " )) * (tan . (x + h))) - ((tan . x) * (tan . x)) by A2, RFUNCT_1:def 4
.= (((sin . (x + h)) * ((cos . (x + h)) " )) * ((sin . (x + h)) * ((cos . (x + h)) " ))) - ((tan . x) * (tan . x)) by A2, RFUNCT_1:def 4
.= (((sin . (x + h)) * ((cos . (x + h)) " )) * ((sin . (x + h)) * ((cos . (x + h)) " ))) - (((sin . x) * ((cos . x) " )) * (tan . x)) by A2, RFUNCT_1:def 4
.= ((tan (x + h)) ^2 ) - ((tan x) ^2 ) by A2, RFUNCT_1:def 4
.= ((tan (x + h)) - (tan x)) * ((tan (x + h)) + (tan x))
.= ((sin ((x + h) - x)) / ((cos (x + h)) * (cos x))) * ((tan (x + h)) + (tan x)) by A3, SIN_COS4:24
.= ((sin ((x + h) - x)) / ((cos (x + h)) * (cos x))) * ((sin ((x + h) + x)) / ((cos (x + h)) * (cos x))) by A3, SIN_COS4:23
.= ((sin ((2 * x) + h)) * (sin h)) / (((cos (x + h)) * (cos x)) ^2 ) by XCMPLX_1:77
.= (- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))))) / (((cos (x + h)) * (cos x)) ^2 ) by SIN_COS4:33
.= - (((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((cos (x + h)) * (cos x)) ^2 )) ;
hence (fD f,h) . x = - (((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((cos (x + h)) * (cos x)) ^2 )) ; :: thesis: verum