let r be Real; :: thesis: ( - (sqrt 2) <= r & r <= - 1 implies ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2 ) - 1)) / r) ) )
set x = arccosec1 r;
assume A1: ( - (sqrt 2) <= r & r <= - 1 ) ; :: thesis: ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2 ) - 1)) / r) )
then r in [.(- (sqrt 2)),(- 1).] ;
then A2: arccosec1 r in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) by Lm15, Th87;
A3: dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) c= dom cosec by RELAT_1:89;
A8: r = (sin ^ ) . (arccosec1 r) by A1, Th91
.= 1 / (sin . (arccosec1 r)) by A2, A3, RFUNCT_1:def 8 ;
r < 0 by A1;
then A10: r ^2 > 0 ;
((sin . (arccosec1 r)) ^2 ) + ((cos . (arccosec1 r)) ^2 ) = 1 by SIN_COS:31;
then A11: (cos . (arccosec1 r)) ^2 = 1 - ((sin . (arccosec1 r)) ^2 )
.= 1 - ((1 / r) * (1 / r)) by A8
.= 1 - (1 / (r ^2 )) by XCMPLX_1:103
.= ((r ^2 ) / (r ^2 )) - (1 / (r ^2 )) by A10, XCMPLX_1:60
.= ((r ^2 ) - 1) / (r ^2 ) ;
- r >= - (- 1) by A1, XREAL_1:26;
then (- r) ^2 >= 1 ^2 by SQUARE_1:77;
then A12: (r ^2 ) - 1 >= 0 by XREAL_1:50;
A14: - (PI / 2) in [.(- (PI / 2)),(PI / 2).] ;
A15: ( - (PI / 4) >= - (PI / 2) & - (PI / 4) < 0 ) by Lm11, XXREAL_1:3;
- (PI / 4) in [.(- (PI / 2)),(PI / 2).] by A15;
then [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),(PI / 2).] by A14, XXREAL_2:def 12;
then cos . (arccosec1 r) >= 0 by A2, Lm15, COMPTRIG:28;
then cos . (arccosec1 r) = sqrt (((r ^2 ) - 1) / (r ^2 )) by A11, SQUARE_1:def 4
.= (sqrt ((r ^2 ) - 1)) / (sqrt (r ^2 )) by A10, A12, SQUARE_1:99
.= (sqrt ((r ^2 ) - 1)) / (- r) by A1, SQUARE_1:90
.= - ((sqrt ((r ^2 ) - 1)) / r) by XCMPLX_1:189 ;
hence ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2 ) - 1)) / r) ) by A8; :: thesis: verum