let r be Real; :: thesis: ( not sin r = 0 or r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) )
set i = [\(r / (2 * PI))/];
assume A1: sin r = 0 ; :: thesis: ( r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((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;
sin w = sin r by A2, COMPLEX2:8;
then ( w = 0 or w = PI ) by A1, A3, A4, COMPTRIG:17;
hence ( r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) by A2; :: thesis: verum