let r be Real; :: thesis: ( not cos r = 0 or r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) )
set i = [\(r / (2 * PI))/];
assume A1: cos r = 0 ; :: thesis: ( r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) )
consider w being Real such that
A2: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + r and
A3: 0 <= w and
A4: w < 2 * PI by COMPLEX2:1;
cos w = cos r by A2, COMPLEX2:9;
then ( w = PI / 2 or w = (3 * PI) / 2 ) by A1, A3, A4, COMPTRIG:18;
hence ( r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) ) by A2; :: thesis: verum