let r be Real; ( 0 <= r & r <= PI / 2 & r / PI is rational & cos r is rational implies r in {0,(PI / 3),(PI / 2)} )
assume that
A1:
0 <= r
and
A2:
r <= PI / 2
and
A3:
r / PI is rational
and
A4:
cos r is rational
; r in {0,(PI / 3),(PI / 2)}
consider k being Integer, n being Nat such that
A5:
n <> 0
and
A6:
(r / PI) / 2 = k / n
by A3, RAT_1:8;
set e = 2 * (cos r);
reconsider c = 2 * (cos r) as Element of F_Real by XREAL_0:def 1;
consider p being INT -valued monic Polynomial of F_Real such that
A7:
eval (p,c) = 2 * (cos (n * r))
and
A8:
deg p = n
and
( ( n = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( n = 2 implies ex a being Element of F_Real st
( a = - 2 & p = <%a,(0. F_Real),(1. F_Real)%> ) ) )
by A5, NAT_1:14, Th52;
A9:
n * (((2 * PI) * k) / n) = (2 * PI) * k
by A5, XCMPLX_1:87;
A10:
cos (((2 * PI) * k) + 0) = 1
by SIN_COS:31, COMPLEX2:9;
reconsider r2 = 2 as Element of F_Real by XREAL_0:def 1;
(r / PI) / 2 = r / (2 * PI)
by XCMPLX_1:78;
then
r = ((2 * PI) * k) / n
by A6, Th1;
then A11:
c is_a_root_of p - <%r2%>
by A7, A9, A10, Th47;
(len <%r2%>) - 1 <= 1 - 1
by XREAL_1:9, ALGSEQ_1:def 5;
then
deg p > deg <%r2%>
by A5, A8;
then
p - <%r2%> is monic
by Th46;
then A12:
2 * (cos r) is integer
by A4, A11, Th51;
PI / 2 < 2 * PI
by XREAL_1:68;
then A13:
r < 2 * PI
by A2, XXREAL_0:2;
A14:
r in [.(- (PI / 2)),(PI / 2).]
by A1, A2, XXREAL_1:1;
cos . r in [.(- 1),1.]
by COMPTRIG:27;
then
( - 1 <= cos r & cos r <= 1 )
by XXREAL_1:1;
then
( 2 * (- 1) <= 2 * (cos r) & 2 * (cos r) <= 2 * 1 )
by XREAL_1:64;
then
( - 2 <= 2 * (cos r) & 2 * (cos r) <= 2 )
;
then
|.(2 * (cos r)).| <= 2
by ABSVALUE:5;
then
( 2 * (cos r) = - 2 or 2 * (cos r) = - 1 or 2 * (cos r) = 0 or 2 * (cos r) = 1 or 2 * (cos r) = 2 )
by A12, Th3;
then
( cos r = - 1 or cos r = - (1 / 2) or cos r = 0 or cos r = 1 / 2 or cos r = 1 )
;
then
( r = PI / 2 or r = (3 / 2) * PI or r = PI / 3 or r = 0 )
by A1, A2, A13, A14, Th15, COMPTRIG:12, COMPTRIG:18, COMPTRIG:61;
hence
r in {0,(PI / 3),(PI / 2)}
by A2, XREAL_1:68, ENUMSET1:def 1; verum