let r be Real; :: thesis: ( cos r = - 1 implies r = PI + ((2 * PI) * [\(r / (2 * PI))/]) )
set i = [\(r / (2 * PI))/];
consider w being Real such that
A1: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + r and
A2: ( 0 <= w & w < 2 * PI ) by COMPLEX2:1;
assume A3: cos r = - 1 ; :: thesis: r = PI + ((2 * PI) * [\(r / (2 * PI))/])
then ((sin r) * (sin r)) + ((- 1) * (- 1)) = 1 by SIN_COS:29;
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:6;
then ( r = 0 + H₁([\(r / (2 * PI))/]) or r = PI + H₁([\(r / (2 * PI))/]) ) by A1, A4, Th21;
hence r = PI + ((2 * PI) * [\(r / (2 * PI))/]) by A3, COMPLEX2:9, SIN_COS:31; :: thesis: verum