let Z be open Subset of REAL ; :: thesis: ( Z c= dom tan implies ( tan is_differentiable_on Z & tan `| Z = ((cos ^ ) ^2 ) | Z ) )
assume A1:
Z c= dom tan
; :: thesis: ( tan is_differentiable_on Z & tan `| Z = ((cos ^ ) ^2 ) | Z )
A2:
for x being Real st x in Z holds
tan is_differentiable_in x
then A7:
tan is_differentiable_on Z
by A1, FDIFF_1:16;
then B1:
dom (tan `| Z) = Z
by FDIFF_1:def 8;
set f1 = cos ^ ;
AA: dom tan =
dom (sin (#) (cos ^ ))
by RFUNCT_1:47, SIN_COS:def 30
.=
(dom sin ) /\ (dom (cos ^ ))
by VALUED_1:def 4
;
c1:
(dom sin ) /\ (dom (cos ^ )) c= dom (cos ^ )
by XBOOLE_1:17;
then C1:
Z c= dom (cos ^ )
by A1, AA, XBOOLE_1:1;
C2: dom ((cos ^ ) (#) (cos ^ )) =
(dom (cos ^ )) /\ (dom (cos ^ ))
by VALUED_1:def 4
.=
dom (cos ^ )
;
C3: dom (((cos ^ ) (#) (cos ^ )) | Z) =
(dom (cos ^ )) /\ Z
by C2, RELAT_1:90
.=
Z
by c1, A1, AA, XBOOLE_1:1, XBOOLE_1:28
;
for x being Real st x in dom (tan `| Z) holds
(tan `| Z) . x = (((cos ^ ) (#) (cos ^ )) | Z) . x
proof
let x be
Real;
:: thesis: ( x in dom (tan `| Z) implies (tan `| Z) . x = (((cos ^ ) (#) (cos ^ )) | Z) . x )
assume B4:
x in dom (tan `| Z)
;
:: thesis: (tan `| Z) . x = (((cos ^ ) (#) (cos ^ )) | Z) . x
A8:
x in Z
by B4, A7, FDIFF_1:def 8;
A12:
cos . x <> 0
by A1, A8, FDIFF_8:1;
(tan `| Z) . x =
diff (sin / cos ),
x
by A7, A8, FDIFF_1:def 8, SIN_COS:def 30
.=
1
/ ((cos . x) ^2 )
by A12, FDIFF_7:46
.=
(1 / (cos . x)) * (1 / (cos . x))
by XCMPLX_1:103
.=
(1 * ((cos . x) " )) * (1 / (cos . x))
by XCMPLX_0:def 9
.=
((cos ^ ) . x) * (1 / (cos . x))
by A8, C1, RFUNCT_1:def 8
.=
((cos ^ ) . x) * (1 * ((cos . x) " ))
by XCMPLX_0:def 9
.=
((cos ^ ) . x) * ((cos ^ ) . x)
by A8, C1, RFUNCT_1:def 8
.=
((cos ^ ) (#) (cos ^ )) . x
by A8, C1, C2, VALUED_1:def 4
.=
(((cos ^ ) (#) (cos ^ )) | Z) . x
by A8, FUNCT_1:72
;
hence
(tan `| Z) . x = (((cos ^ ) (#) (cos ^ )) | Z) . x
;
:: thesis: verum
end;
hence
( tan is_differentiable_on Z & tan `| Z = ((cos ^ ) ^2 ) | Z )
by B1, C3, A1, A2, FDIFF_1:16, PARTFUN1:34; :: thesis: verum