let r be real number ; :: thesis: ( - 1 <= r & r <= 1 implies ( 0 <= (arccos r) / (2 * PI ) & (arccos r) / (2 * PI ) <= 1 / 2 ) )
assume that
A1: - 1 <= r and
A2: r <= 1 ; :: thesis: ( 0 <= (arccos r) / (2 * PI ) & (arccos r) / (2 * PI ) <= 1 / 2 )
arccos r <= PI by A1, A2, SIN_COS6:101;
then A3: (arccos r) / (2 * PI ) <= (1 * PI ) / (2 * PI ) by XREAL_1:74;
0 <= arccos r by A1, A2, SIN_COS6:101;
hence ( 0 <= (arccos r) / (2 * PI ) & (arccos r) / (2 * PI ) <= 1 / 2 ) by A3, XCMPLX_1:92; :: thesis: verum