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