let r be Real; :: thesis: for i being Integer st (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) holds
sin r >= 0
let i be Integer; :: thesis: ( (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) implies sin r >= 0 )
assume A1: ( (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) ) ; :: thesis: sin r >= 0
per cases ( ( (2 * PI) * i < r & r < PI + ((2 * PI) * i) ) or (2 * PI) * i = r or r = PI + ((2 * PI) * i) ) by A1, XXREAL_0:1;
suppose ( (2 * PI) * i < r & r < PI + ((2 * PI) * i) ) ; :: thesis: sin r >= 0
hence sin r >= 0 by Th11; :: thesis: verum
end;
suppose A2: (2 * PI) * i = r ; :: thesis: sin r >= 0
sin (0 + ((2 * PI) * i)) = sin 0 by COMPLEX2:8;
hence sin r >= 0 by A2, SIN_COS:31; :: thesis: verum
end;
suppose r = PI + ((2 * PI) * i) ; :: thesis: sin r >= 0
hence sin r >= 0 by COMPLEX2:8, SIN_COS:77; :: thesis: verum
end;
end;