let r be Real; ( - (sqrt 2) <= r & r <= - 1 implies ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) ) )
set x = arccosec1 r;
assume that
A1:
- (sqrt 2) <= r
and
A2:
r <= - 1
; ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) )
r in [.(- (sqrt 2)),(- 1).]
by A1, A2;
then A3:
arccosec1 r in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).])
by Lm31, Th87;
- (PI / 4) >= - (PI / 2)
by Lm7, XXREAL_1:3;
then
( - (PI / 2) in [.(- (PI / 2)),(PI / 2).] & - (PI / 4) in [.(- (PI / 2)),(PI / 2).] )
;
then
[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),(PI / 2).]
by XXREAL_2:def 12;
then A4:
cos . (arccosec1 r) >= 0
by A3, Lm31, COMPTRIG:12;
A5:
dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) c= dom cosec
by RELAT_1:60;
A6: r =
(sin ^) . (arccosec1 r)
by A1, A2, Th91
.=
1 / (sin . (arccosec1 r))
by A3, A5, RFUNCT_1:def 2
;
- r >= - (- 1)
by A2, XREAL_1:24;
then
(- r) ^2 >= 1 ^2
by SQUARE_1:15;
then A7:
(r ^2) - 1 >= 0
by XREAL_1:48;
((sin . (arccosec1 r)) ^2) + ((cos . (arccosec1 r)) ^2) = 1
by SIN_COS:28;
then (cos . (arccosec1 r)) ^2 =
1 - ((sin . (arccosec1 r)) ^2)
.=
1 - ((1 / r) * (1 / r))
by A6
.=
1 - (1 / (r ^2))
by XCMPLX_1:102
.=
((r ^2) / (r ^2)) - (1 / (r ^2))
by A2, XCMPLX_1:60
.=
((r ^2) - 1) / (r ^2)
;
then cos . (arccosec1 r) =
sqrt (((r ^2) - 1) / (r ^2))
by A4, SQUARE_1:def 2
.=
(sqrt ((r ^2) - 1)) / (sqrt (r ^2))
by A2, A7, SQUARE_1:30
.=
(sqrt ((r ^2) - 1)) / (- r)
by A2, SQUARE_1:23
.=
- ((sqrt ((r ^2) - 1)) / r)
by XCMPLX_1:188
;
hence
( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) )
by A6; verum