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