let Z be open Subset of REAL; ( Z c= dom tan implies ( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z ) )
A1:
(dom sin) /\ (dom (cos ^)) c= dom (cos ^)
by XBOOLE_1:17;
assume A2:
Z c= dom tan
; ( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z )
then A3:
for x being Real st x in Z holds
cos . x <> 0
by FDIFF_8:1;
then
cos ^ is_differentiable_on Z
by FDIFF_4:39;
then A4:
dom ((cos ^) `| Z) = Z
by FDIFF_1:def 7;
dom tan =
dom (sin (#) (cos ^))
by RFUNCT_1:31, SIN_COS:def 26
.=
(dom sin) /\ (dom (cos ^))
by VALUED_1:def 4
;
then A5:
Z c= dom (cos ^)
by A2, A1;
A6:
for x being Element of REAL st x in Z holds
((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x
proof
let x be
Element of
REAL ;
( x in Z implies ((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x )
A7:
dom ((cos ^) (#) sin) = dom tan
by RFUNCT_1:31, SIN_COS:def 26;
then
dom (((cos ^) (#) sin) (#) (cos ^)) = (dom tan) /\ (dom (cos ^))
by VALUED_1:def 4;
then A8:
Z c= dom (((cos ^) (#) sin) (#) (cos ^))
by A2, A5, XBOOLE_1:19;
assume A9:
x in Z
;
((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x
then ((cos ^) `| Z) . x =
(sin . x) / ((cos . x) ^2)
by A3, FDIFF_4:39
.=
(1 / (cos . x)) * ((sin . x) / (cos . x))
by XCMPLX_1:103
.=
((1 / (cos . x)) * (sin . x)) * (1 / (cos . x))
by XCMPLX_1:99
.=
((1 / (cos . x)) * (sin . x)) * (1 * ((cos . x) "))
by XCMPLX_0:def 9
.=
((1 * ((cos . x) ")) * (sin . x)) * (1 * ((cos . x) "))
by XCMPLX_0:def 9
.=
(((cos ^) . x) * (sin . x)) * (1 * ((cos . x) "))
by A5, A9, RFUNCT_1:def 2
.=
(((cos ^) . x) * (sin . x)) * ((cos ^) . x)
by A5, A9, RFUNCT_1:def 2
.=
(((cos ^) (#) sin) . x) * ((cos ^) . x)
by A2, A9, A7, VALUED_1:def 4
.=
(((cos ^) (#) sin) (#) (cos ^)) . x
by A9, A8, VALUED_1:def 4
.=
((((cos ^) (#) sin) (#) (cos ^)) | Z) . x
by A9, FUNCT_1:49
.=
(((cos ^) (#) tan) | Z) . x
by RFUNCT_1:31, SIN_COS:def 26
;
hence
((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x
;
verum
end;
dom (((cos ^) (#) tan) | Z) =
(dom ((cos ^) (#) tan)) /\ Z
by RELAT_1:61
.=
((dom (cos ^)) /\ (dom tan)) /\ Z
by VALUED_1:def 4
.=
Z
by A2, A5, XBOOLE_1:19, XBOOLE_1:28
;
hence
( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z )
by A3, A4, A6, FDIFF_4:39, PARTFUN1:5; verum