let r be real number ; :: thesis: ( cos ((2 * PI ) * r) = 1 implies r in INT )
assume A1: cos ((2 * PI ) * r) = 1 ; :: thesis: r in INT
set s = [\r/];
assume not r in INT ; :: thesis: contradiction
then not r is integer by INT_1:def 2;
then reconsider t = frac r as real positive number by INT_1:72;
A2: r = [\r/] + t by INT_1:68;
A3: cos ((2 * PI ) * ([\r/] + t)) = cos (((2 * PI ) * [\r/]) + ((2 * PI ) * t))
.= cos ((2 * PI ) * t) by COMPLEX2:10 ;
reconsider d = 2 as real positive number ;
t < 1 by INT_1:69;
then (d * PI ) * t < (d * PI ) * 1 by XREAL_1:70;
hence contradiction by A1, A2, A3, Th34; :: thesis: verum