let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies arcsin r = - (arcsin (- r)) )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: arcsin r = - (arcsin (- r))
then A1: ( - (- 1) >= - r & - r >= - 1 ) by XREAL_1:24;
then arcsin (- r) <= PI / 2 by Th76;
then A2: - (PI / 2) <= - (arcsin (- r)) by XREAL_1:24;
- (PI / 2) <= arcsin (- r) by A1, Th76;
then A3: - (arcsin (- r)) <= - (- (PI / 2)) by XREAL_1:24;
r = 0 - (1 * (- r))
.= ((sin 0) * (cos (arcsin (- r)))) - ((cos 0) * (sin (arcsin (- r)))) by A1, Th68, SIN_COS:31
.= sin (0 - (arcsin (- r))) by COMPLEX2:3 ;
hence arcsin r = - (arcsin (- r)) by A2, A3, Th69; :: thesis: verum