let r be Real; :: thesis: ( - (sqrt 2) <= r & r <= - 1 implies ( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r ) )
(3 / 4) * PI <= PI by Lm6, XXREAL_1:2;
then A1: (3 / 4) * PI in [.0,PI.] ;
A2: dom (sec | [.((3 / 4) * PI),PI.]) c= dom sec by RELAT_1:60;
set x = arcsec2 r;
assume that
A3: - (sqrt 2) <= r and
A4: r <= - 1 ; :: thesis: ( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r )
r in [.(- (sqrt 2)),(- 1).] by A3, A4;
then A5: arcsec2 r in dom (sec | [.((3 / 4) * PI),PI.]) by Lm30, Th86;
A6: r = (cos ^) . (arcsec2 r) by A3, A4, Th90
.= 1 / (cos . (arcsec2 r)) by A5, A2, RFUNCT_1:def 2 ;
PI in [.0,PI.] ;
then [.((3 / 4) * PI),PI.] c= [.0,PI.] by A1, XXREAL_2:def 12;
then A7: sin . (arcsec2 r) >= 0 by A5, Lm30, COMPTRIG:8;
- r >= - (- 1) by A4, XREAL_1:24;
then (- r) ^2 >= 1 ^2 by SQUARE_1:15;
then A8: (r ^2) - 1 >= 0 by XREAL_1:48;
((sin . (arcsec2 r)) ^2) + ((cos . (arcsec2 r)) ^2) = 1 by SIN_COS:28;
then (sin . (arcsec2 r)) ^2 = 1 - ((cos . (arcsec2 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 A4, XCMPLX_1:60
.= ((r ^2) - 1) / (r ^2) ;
then sin . (arcsec2 r) = sqrt (((r ^2) - 1) / (r ^2)) by A7, SQUARE_1:def 2
.= (sqrt ((r ^2) - 1)) / (sqrt (r ^2)) by A4, A8, SQUARE_1:30
.= (sqrt ((r ^2) - 1)) / (- r) by A4, SQUARE_1:23
.= - ((sqrt ((r ^2) - 1)) / r) by XCMPLX_1:188 ;
hence ( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r ) by A6; :: thesis: verum