let r be Real; ( 1 <= r & r <= sqrt 2 implies ( sin . (arcsec1 r) = (sqrt ((r ^2 ) - 1)) / r & cos . (arcsec1 r) = 1 / r ) )
set x = arcsec1 r;
assume that
A1:
1 <= r
and
A2:
r <= sqrt 2
; ( sin . (arcsec1 r) = (sqrt ((r ^2 ) - 1)) / r & cos . (arcsec1 r) = 1 / r )
r in [.1,(sqrt 2).]
by A1, A2;
then A3:
arcsec1 r in dom (sec | [.0 ,(PI / 4).])
by Lm29, Th85;
PI / 4 < PI / 1
by XREAL_1:78;
then
( 0 in [.0 ,PI .] & PI / 4 in [.0 ,PI .] )
;
then
[.0 ,(PI / 4).] c= [.0 ,PI .]
by XXREAL_2:def 12;
then A4:
sin . (arcsec1 r) >= 0
by A3, Lm29, COMPTRIG:24;
A5:
dom (sec | [.0 ,(PI / 4).]) c= dom sec
by RELAT_1:89;
A6: r =
(cos ^ ) . (arcsec1 r)
by A1, A2, Th89
.=
1 / (cos . (arcsec1 r))
by A3, A5, RFUNCT_1:def 8
;
r ^2 >= 1 ^2
by A1, SQUARE_1:77;
then A7:
(r ^2 ) - 1 >= 0
by XREAL_1:50;
((sin . (arcsec1 r)) ^2 ) + ((cos . (arcsec1 r)) ^2 ) = 1
by SIN_COS:31;
then (sin . (arcsec1 r)) ^2 =
1 - ((cos . (arcsec1 r)) ^2 )
.=
1 - ((1 / r) * (1 / r))
by A6
.=
1 - (1 / (r ^2 ))
by XCMPLX_1:103
.=
((r ^2 ) / (r ^2 )) - (1 / (r ^2 ))
by A1, XCMPLX_1:60
.=
((r ^2 ) - 1) / (r ^2 )
;
then sin . (arcsec1 r) =
sqrt (((r ^2 ) - 1) / (r ^2 ))
by A4, SQUARE_1:def 4
.=
(sqrt ((r ^2 ) - 1)) / (sqrt (r ^2 ))
by A1, A7, SQUARE_1:99
.=
(sqrt ((r ^2 ) - 1)) / r
by A1, SQUARE_1:89
;
hence
( sin . (arcsec1 r) = (sqrt ((r ^2 ) - 1)) / r & cos . (arcsec1 r) = 1 / r )
by A6; verum