let r be real number ; :: thesis: ( cos ((2 * PI ) * r) = 1 implies r in INT )
reconsider d = 2 as real positive number ;
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 real positive number by INT_1:72;
set s = [\r/];
A2: ( r = [\r/] + t & (d * PI ) * t < (d * PI ) * 1 ) by INT_1:68, INT_1:69, XREAL_1:70;
cos ((2 * PI ) * ([\r/] + t)) = cos (((2 * PI ) * [\r/]) + ((2 * PI ) * t))
.= cos ((2 * PI ) * t) by COMPLEX2:10 ;
hence contradiction by A1, A2, Th34; :: thesis: verum