let r, s be Real; :: thesis: for i being Integer st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s & s < (2 * PI) + ((2 * PI) * i) & sin r = sin s & cos r = cos s holds
r = s
let i be Integer; :: thesis: ( (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s & s < (2 * PI) + ((2 * PI) * i) & sin r = sin s & cos r = cos s implies r = s )
assume that
A1: (2 * PI) * i <= r and
A2: ( r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s ) and
A3: s < (2 * PI) + ((2 * PI) * i) and
A4: ( sin r = sin s & cos r = cos s ) ; :: thesis: r = s
A5: cos (r - s) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by COMPLEX2:3
.= 1 by A4, SIN_COS:29 ;
A6: sin (r - s) = ((sin r) * (cos s)) - ((cos r) * (sin s)) by COMPLEX2:3
.= 0 by A4 ;
A7: cos (s - r) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by COMPLEX2:3
.= 1 by A4, SIN_COS:29 ;
A8: sin (s - r) = ((sin s) * (cos r)) - ((cos s) * (sin r)) by COMPLEX2:3
.= 0 by A4 ;
per cases ( r > s or r < s or r = s ) by XXREAL_0:1;
suppose A9: r > s ; :: thesis: r = s
r + ((2 * PI) * i) < ((2 * PI) + ((2 * PI) * i)) + s by A2, XREAL_1:8;
then (r + ((2 * PI) * i)) - ((2 * PI) * i) < (((2 * PI) + ((2 * PI) * i)) + s) - ((2 * PI) * i) by XREAL_1:9;
then r < (2 * PI) + s ;
then A10: r - s < 2 * PI by XREAL_1:19;
r > s + 0 by A9;
then 0 <= r - s by XREAL_1:20;
then ( r - s = 0 or r - s = PI ) by A6, A10, COMPTRIG:17;
hence r = s by A5, SIN_COS:77; :: thesis: verum
end;
suppose A11: r < s ; :: thesis: r = s
s + ((2 * PI) * i) < ((2 * PI) + ((2 * PI) * i)) + r by A1, A3, XREAL_1:8;
then (s + ((2 * PI) * i)) - ((2 * PI) * i) < (((2 * PI) + ((2 * PI) * i)) + r) - ((2 * PI) * i) by XREAL_1:9;
then s < (2 * PI) + r ;
then A12: s - r < 2 * PI by XREAL_1:19;
s > r + 0 by A11;
then 0 <= s - r by XREAL_1:20;
then ( s - r = 0 or s - r = PI ) by A8, A12, COMPTRIG:17;
hence r = s by A7, SIN_COS:77; :: thesis: verum
end;
suppose r = s ; :: thesis: r = s
hence r = s ; :: thesis: verum
end;
end;