let Z be open Subset of REAL ; :: thesis: ( Z c= dom (tan - (id Z)) implies ( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2 ) ) )
assume A1:
Z c= dom (tan - (id Z))
; :: thesis: ( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2 ) )
then
Z c= (dom tan ) /\ (dom (id Z))
by VALUED_1:12;
then A2:
( Z c= dom tan & Z c= dom (id Z) )
by XBOOLE_1:18;
A3:
for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0
by FUNCT_1:35;
then A4:
( id Z is_differentiable_on Z & ( for x being Real st x in Z holds
((id Z) `| Z) . x = 1 ) )
by A2, FDIFF_1:31;
for x being Real st x in Z holds
tan is_differentiable_in x
then A5:
tan is_differentiable_on Z
by A2, FDIFF_1:16;
for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2
proof
let x be
Real;
:: thesis: ( x in Z implies ((tan - (id Z)) `| Z) . x = (tan . x) ^2 )
assume A6:
x in Z
;
:: thesis: ((tan - (id Z)) `| Z) . x = (tan . x) ^2
then A7:
cos . x <> 0
by A2, FDIFF_8:1;
then A8:
(cos . x) ^2 > 0
by SQUARE_1:74;
((tan - (id Z)) `| Z) . x =
(diff tan ,x) - (diff (id Z),x)
by A1, A4, A5, A6, FDIFF_1:27
.=
(1 / ((cos . x) ^2 )) - (diff (id Z),x)
by A7, FDIFF_7:46
.=
(1 / ((cos . x) ^2 )) - (((id Z) `| Z) . x)
by A4, A6, FDIFF_1:def 8
.=
(1 / ((cos . x) ^2 )) - 1
by A2, A3, A6, FDIFF_1:31
.=
(1 / ((cos . x) ^2 )) - (((cos . x) ^2 ) / ((cos . x) ^2 ))
by A8, XCMPLX_1:60
.=
(1 - ((cos . x) ^2 )) / ((cos . x) ^2 )
by XCMPLX_1:121
.=
((((sin . x) ^2 ) + ((cos . x) ^2 )) - ((cos . x) ^2 )) / ((cos . x) ^2 )
by SIN_COS:31
.=
((sin x) / (cos x)) * ((sin . x) / (cos . x))
by XCMPLX_1:77
.=
(tan . x) * (tan x)
by A2, A6, FDIFF_8:1, SIN_COS9:15
.=
(tan . x) ^2
by A2, A6, FDIFF_8:1, SIN_COS9:15
;
hence
((tan - (id Z)) `| Z) . x = (tan . x) ^2
;
:: thesis: verum
end;
hence
( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2 ) )
by A1, A4, A5, FDIFF_1:27; :: thesis: verum