let Z be open Subset of REAL; ( Z c= dom tan & Z c= ].(- 1),1.[ implies ( tan (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2) ) ) )
assume that
A1:
Z c= dom tan
and
A2:
Z c= ].(- 1),1.[
; ( tan (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2) ) )
A3:
arctan + arccot is_differentiable_on Z
by A2, Th37;
for x being Real st x in Z holds
tan is_differentiable_in x
then A4:
tan is_differentiable_on Z
by A1, FDIFF_1:9;
A5:
].(- 1),1.[ c= [.(- 1),1.]
by XXREAL_1:25;
then
].(- 1),1.[ c= dom arccot
by SIN_COS9:24, XBOOLE_1:1;
then A6:
Z c= dom arccot
by A2, XBOOLE_1:1;
].(- 1),1.[ c= dom arctan
by A5, SIN_COS9:23, XBOOLE_1:1;
then
Z c= dom arctan
by A2, XBOOLE_1:1;
then
Z c= (dom arctan) /\ (dom arccot)
by A6, XBOOLE_1:19;
then A7:
Z c= dom (arctan + arccot)
by VALUED_1:def 1;
then
Z c= (dom tan) /\ (dom (arctan + arccot))
by A1, XBOOLE_1:19;
then A8:
Z c= dom (tan (#) (arctan + arccot))
by VALUED_1:def 4;
for x being Real st x in Z holds
((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2)
proof
let x be
Real;
( x in Z implies ((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2) )
assume A9:
x in Z
;
((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2)
then A10:
cos . x <> 0
by A1, FDIFF_8:1;
((tan (#) (arctan + arccot)) `| Z) . x =
(((arctan + arccot) . x) * (diff (tan,x))) + ((tan . x) * (diff ((arctan + arccot),x)))
by A8, A4, A3, A9, FDIFF_1:21
.=
(((arctan . x) + (arccot . x)) * (diff (tan,x))) + ((tan . x) * (diff ((arctan + arccot),x)))
by A7, A9, VALUED_1:def 1
.=
(((arctan . x) + (arccot . x)) * (1 / ((cos . x) ^2))) + ((tan . x) * (diff ((arctan + arccot),x)))
by A10, FDIFF_7:46
.=
(((arctan . x) + (arccot . x)) / ((cos . x) ^2)) + ((tan . x) * (((arctan + arccot) `| Z) . x))
by A3, A9, FDIFF_1:def 7
.=
(((arctan . x) + (arccot . x)) / ((cos . x) ^2)) + ((tan . x) * 0)
by A2, A9, Th37
.=
((arctan . x) + (arccot . x)) / ((cos . x) ^2)
;
hence
((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2)
;
verum
end;
hence
( tan (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2) ) )
by A8, A4, A3, FDIFF_1:21; verum