let r be Real; :: thesis: for i being Integer st (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) holds
cos r >= 0
let i be Integer; :: thesis: ( (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) implies cos r >= 0 )
assume ( (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) ) ; :: thesis: cos r >= 0
then ( ( (- (PI / 2)) + ((2 * PI) * i) < r & r < (PI / 2) + ((2 * PI) * i) ) or (- (PI / 2)) + ((2 * PI) * i) = r or r = (PI / 2) + ((2 * PI) * i) ) by XXREAL_0:1;
hence cos r >= 0 by Th9, Th13, COMPLEX2:9, SIN_COS:77; :: thesis: verum