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