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