let r be Real; :: thesis: ( - (sqrt 2) < r & r < - 1 implies cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1))) )
set x = arcsec2 r;
A1: ].((3 / 4) * PI),PI.[ c= dom cosec
proof
].((3 / 4) * PI),PI.[ /\ (sin " {0}) = {}
proof
assume ].((3 / 4) * PI),PI.[ /\ (sin " {0}) <> {} ; :: thesis: contradiction
then consider rr being object such that
A2: rr in ].((3 / 4) * PI),PI.[ /\ (sin " {0}) by XBOOLE_0:def 1;
rr in sin " {0} by A2, XBOOLE_0:def 4;
then A3: sin . rr in {0} by FUNCT_1:def 7;
A4: ].((3 / 4) * PI),PI.[ c= ].0,PI.[ by XXREAL_1:46;
rr in ].((3 / 4) * PI),PI.[ by A2, XBOOLE_0:def 4;
then sin . rr <> 0 by A4, COMPTRIG:7;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum
end;
then ( ].((3 / 4) * PI),PI.[ \ (sin " {0}) c= (dom sin) \ (sin " {0}) & ].((3 / 4) * PI),PI.[ misses sin " {0} ) by SIN_COS:24, XBOOLE_0:def 7, XBOOLE_1:33;
then ].((3 / 4) * PI),PI.[ c= (dom sin) \ (sin " {0}) by XBOOLE_1:83;
hence ].((3 / 4) * PI),PI.[ c= dom cosec by RFUNCT_1:def 2; :: thesis: verum
end;
assume A5: ( - (sqrt 2) < r & r < - 1 ) ; :: thesis: cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1)))
then ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) by Th110;
then arcsec2 r in ].((3 / 4) * PI),PI.[ ;
then cosec . (arcsec2 r) = 1 / (sin . (arcsec2 r)) by A1, RFUNCT_1:def 2
.= 1 / (- ((sqrt ((r ^2) - 1)) / r)) by A5, Th114
.= - (1 / ((sqrt ((r ^2) - 1)) / r)) by XCMPLX_1:188
.= - (r / (sqrt ((r ^2) - 1))) by XCMPLX_1:57 ;
hence cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1))) ; :: thesis: verum