theorem :: NIVEN:17

for i being Integer holds cos (((5 * PI) / 3) + ((2 * PI) * i)) = 1 / 2 by COMPLEX2:9, Th13;