let x be real number ; :: 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 23;
then ( not x in ].(- (PI / 2)),(PI / 2).[ & not x in ].(PI / 2),((3 / 2) * PI ).[ ) by Th27, Th29;
then ( ( - (PI / 2) >= x or x >= PI / 2 ) & ( PI / 2 >= x or x >= (3 / 2) * PI ) ) by XXREAL_1:4;
then ( x = PI / 2 or x = (3 / 2) * PI or x > (3 / 2) * PI ) by A1, Lm0, 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, Th31; :: thesis: verum