let s, r be real number ; :: thesis: ( s <= 0 & (r ^2 ) + (s ^2 ) = 1 implies cos (arcsin r) = - s )
set x = arcsin r;
assume that
A1: s <= 0 and
A2: (r ^2 ) + (s ^2 ) = 1 ; :: thesis: cos (arcsin r) = - s
A3: ( - 1 <= r & r <= 1 ) by A2, Lm7;
((sin . (arcsin r)) ^2 ) + ((cos . (arcsin r)) ^2 ) = 1 by SIN_COS:31;
then (cos . (arcsin r)) ^2 = 1 - ((sin . (arcsin r)) ^2 )
.= 1 - ((sin (arcsin r)) ^2 ) by SIN_COS:def 21
.= 1 - (r ^2 ) by A3, Th69 ;
then A4: ( cos . (arcsin r) = s or cos . (arcsin r) = - s ) by A2, SQUARE_1:109;
( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) by A3, Th77;
then A5: arcsin r in [.(- (PI / 2)),(PI / 2).] by XXREAL_1:1;
( 0 > s or s = 0 ) by A1;
hence cos (arcsin r) = - s by A4, A5, COMPTRIG:28, SIN_COS:def 23; :: thesis: verum