let h, x 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 1
.= (((sin . (x + h)) * ((cos . (x + h)) ")) * ((sin . (x + h)) * ((cos . (x + h)) "))) - ((tan . x) * (tan . x)) by A2, RFUNCT_1:def 1
.= (((sin . (x + h)) * ((cos . (x + h)) ")) * ((sin . (x + h)) * ((cos . (x + h)) "))) - (((sin . x) * ((cos . x) ")) * (tan . x)) by A2, RFUNCT_1:def 1
.= ((tan (x + h)) ^2) - ((tan x) ^2) by A2, RFUNCT_1:def 1
.= ((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:20
.= ((sin ((x + h) - x)) / ((cos (x + h)) * (cos x))) * ((sin ((x + h) + x)) / ((cos (x + h)) * (cos x))) by A3, SIN_COS4:19
.= ((sin ((2 * x) + h)) * (sin h)) / (((cos (x + h)) * (cos x)) ^2) by XCMPLX_1:76
.= (- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))))) / (((cos (x + h)) * (cos x)) ^2) by SIN_COS4:29
.= - (((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