let r be real number ; :: 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:26;
A2: r = 0 - (1 * (- r))
.= ((sin 0 ) * (cos (arcsin (- r)))) - ((cos 0 ) * (sin (arcsin (- r)))) by A1, Th69, SIN_COS:34
.= sin (0 - (arcsin (- r))) by COMPLEX2:4 ;
arcsin (- r) <= PI / 2 by A1, Th77;
then A3: - (PI / 2) <= - (arcsin (- r)) by XREAL_1:26;
- (PI / 2) <= arcsin (- r) by A1, Th77;
then - (arcsin (- r)) <= - (- (PI / 2)) by XREAL_1:26;
hence arcsin r = - (arcsin (- r)) by A2, A3, Th70; :: thesis: verum