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