let Z be open Subset of REAL; ( Z c= dom ((- cot) - (id Z)) implies ( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - (id Z)) `| Z) . x = (cot . x) ^2 ) ) )
set f = - cot;
A1:
for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0
by FUNCT_1:18;
assume A2:
Z c= dom ((- cot) - (id Z))
; ( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - (id Z)) `| Z) . x = (cot . x) ^2 ) )
then
Z c= (dom (- cot)) /\ (dom (id Z))
by VALUED_1:12;
then A3:
Z c= dom (- cot)
by XBOOLE_1:18;
then A4:
Z c= dom cot
by VALUED_1:8;
for x being Real st x in Z holds
cot is_differentiable_in x
then A5:
cot is_differentiable_on Z
by A4, FDIFF_1:9;
then A6:
(- 1) (#) cot is_differentiable_on Z
by A3, FDIFF_1:20;
A7:
Z c= dom (id Z)
;
then A8:
id Z is_differentiable_on Z
by A1, FDIFF_1:23;
for x being Real st x in Z holds
(((- cot) - (id Z)) `| Z) . x = (cot . x) ^2
proof
let x be
Real;
( x in Z implies (((- cot) - (id Z)) `| Z) . x = (cot . x) ^2 )
assume A9:
x in Z
;
(((- cot) - (id Z)) `| Z) . x = (cot . x) ^2
then A10:
sin . x <> 0
by A4, FDIFF_8:2;
then A11:
(sin . x) ^2 > 0
by SQUARE_1:12;
(((- cot) - (id Z)) `| Z) . x =
(diff ((- cot),x)) - (diff ((id Z),x))
by A2, A8, A6, A9, FDIFF_1:19
.=
((((- 1) (#) cot) `| Z) . x) - (diff ((id Z),x))
by A6, A9, FDIFF_1:def 7
.=
((- 1) * (diff (cot,x))) - (diff ((id Z),x))
by A3, A5, A9, FDIFF_1:20
.=
((- 1) * (- (1 / ((sin . x) ^2)))) - (diff ((id Z),x))
by A10, FDIFF_7:47
.=
(1 / ((sin . x) ^2)) - (((id Z) `| Z) . x)
by A8, A9, FDIFF_1:def 7
.=
(1 / ((sin . x) ^2)) - 1
by A7, A1, A9, FDIFF_1:23
.=
(1 / ((sin . x) ^2)) - (((sin . x) ^2) / ((sin . x) ^2))
by A11, XCMPLX_1:60
.=
(1 - ((sin . x) ^2)) / ((sin . x) ^2)
by XCMPLX_1:120
.=
((((cos . x) ^2) + ((sin . x) ^2)) - ((sin . x) ^2)) / ((sin . x) ^2)
by SIN_COS:28
.=
((cos x) / (sin x)) * ((cos . x) / (sin . x))
by XCMPLX_1:76
.=
(cot . x) * (cot x)
by A4, A9, FDIFF_8:2, SIN_COS9:16
.=
(cot . x) ^2
by A4, A9, FDIFF_8:2, SIN_COS9:16
;
hence
(((- cot) - (id Z)) `| Z) . x = (cot . x) ^2
;
verum
end;
hence
( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - (id Z)) `| Z) . x = (cot . x) ^2 ) )
by A2, A8, A6, FDIFF_1:19; verum