let r be real number ; :: thesis: ( cos r = 1 implies r = (2 * PI ) * [\(r / (2 * PI ))/] )
set i = [\(r / (2 * PI ))/];
consider w being real number such that
A1: w = ((2 * PI ) * (- [\(r / (2 * PI ))/])) + r and
A2: ( 0 <= w & w < 2 * PI ) by COMPLEX2:2;
assume A3: cos r = 1 ; :: thesis: r = (2 * PI ) * [\(r / (2 * PI ))/]
then ((sin r) * (sin r)) + (1 * 1) = 1 by SIN_COS:32;
then A4: sin r = 0 ;
( 0 + H₁([\(r / (2 * PI ))/]) <= w + H₁([\(r / (2 * PI ))/]) & w + H₁([\(r / (2 * PI ))/]) < (2 * PI ) + H₁([\(r / (2 * PI ))/]) ) by A2, XREAL_1:8;
then ( r = 0 + H₁([\(r / (2 * PI ))/]) or r = PI + H₁([\(r / (2 * PI ))/]) ) by A1, A4, Th21;
hence r = (2 * PI ) * [\(r / (2 * PI ))/] by A3, COMPLEX2:10, SIN_COS:82; :: thesis: verum