let x be Real; ( 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
; ( 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; verum