let r be Real; :: thesis: ( cos ((2 * PI) * r) = 1 implies r in INT )
reconsider d = 2 as positive Real ;
assume A1: cos ((2 * PI) * r) = 1 ; :: thesis: r in INT
assume not r in INT ; :: thesis: contradiction
then not r is integer by INT_1:def 2;
then reconsider t = frac r as positive Real by INT_1:46;
set s = [\r/];
A2: ( r = [\r/] + t & (d * PI) * t < (d * PI) * 1 ) by INT_1:42, INT_1:43, XREAL_1:68;
cos ((2 * PI) * ([\r/] + t)) = cos (((2 * PI) * [\r/]) + ((2 * PI) * t))
.= cos ((2 * PI) * t) by COMPLEX2:9 ;
hence contradiction by A1, A2, Th34; :: thesis: verum