set f = cot | ].0,PI.[;
A1: dom ((cot | ].0,PI.[) ") =
rng (cot | ].0,PI.[)
by FUNCT_1:33
.=
cot .: ].0,PI.[
by RELAT_1:115
;
dom (cot | ].0,PI.[) = (dom cot) /\ ].0,PI.[
by RELAT_1:61;
then A2:
].0,PI.[ c= dom (cot | ].0,PI.[)
by Th2, XBOOLE_1:19;
A3:
cot | ].0,PI.[ is_differentiable_on ].0,PI.[
by Lm2, FDIFF_2:16;
A4:
now for x0 being Real st x0 in ].0,PI.[ holds
diff ((cot | ].0,PI.[),x0) < 0 A5:
for
x0 being
Real st
x0 in ].0,PI.[ holds
- (1 / ((sin . x0) ^2)) < 0
let x0 be
Real;
( x0 in ].0,PI.[ implies diff ((cot | ].0,PI.[),x0) < 0 )assume A6:
x0 in ].0,PI.[
;
diff ((cot | ].0,PI.[),x0) < 0 diff (
(cot | ].0,PI.[),
x0) =
((cot | ].0,PI.[) `| ].0,PI.[) . x0
by A3, A6, FDIFF_1:def 7
.=
(cot `| ].0,PI.[) . x0
by Lm2, FDIFF_2:16
.=
diff (
cot,
x0)
by A6, Lm2, FDIFF_1:def 7
.=
- (1 / ((sin . x0) ^2))
by A6, Lm4
;
hence
diff (
(cot | ].0,PI.[),
x0)
< 0
by A6, A5;
verum end;
(cot | ].0,PI.[) | ].0,PI.[ = cot | ].0,PI.[
by RELAT_1:72;
hence
arccot is_differentiable_on cot .: ].0,PI.[
by A1, A2, A3, A4, FDIFF_2:48; verum