let x be Real; :: thesis: ( 0 <= x & x < 2 * PI & cos x = 0 & not x = PI / 2 implies x = (3 / 2) * PI )
assume that
A1: 0 <= x and
A2: x < 2 * PI and
A3: cos x = 0 ; :: thesis: ( x = PI / 2 or x = (3 / 2) * PI )
A4: cos . x = 0 by A3, SIN_COS:def 19;
then not x in ].(PI / 2),((3 / 2) * PI).[ by Th13;
then A5: ( PI / 2 >= x or x >= (3 / 2) * PI ) by XXREAL_1:4;
not x in ].(- (PI / 2)),(PI / 2).[ by A4, Th11;
then ( - (PI / 2) >= x or x >= PI / 2 ) by XXREAL_1:4;
then ( x = PI / 2 or x = (3 / 2) * PI or x > (3 / 2) * PI ) by A1, A5, Lm1, XXREAL_0:1;
then ( x = PI / 2 or x = (3 / 2) * PI or x in ].((3 / 2) * PI),(2 * PI).[ ) by A2, XXREAL_1:4;
hence ( x = PI / 2 or x = (3 / 2) * PI ) by A4, Th15; :: thesis: verum