thus A1: 0 < PI / 2 :: thesis: ( PI / 2 < PI & PI < (3 / 2) * PI & (3 / 2) * PI < 2 * PI )

proof

PI in ].0 ,4.[ by SIN_COS:def 32;
then ( 0 < PI & PI < 4 ) by XXREAL_1:4;
then 0 / 2 < PI / 2 by XREAL_1:76;
hence 0 < PI / 2 ; :: thesis: verum

end;

thus A2: PI / 2 < PI :: thesis: ( PI < (3 / 2) * PI & (3 / 2) * PI < 2 * PI )

proof

0 + (PI / 2) < (PI / 2) + (PI / 2) by A1, XREAL_1:8;
hence PI / 2 < PI ; :: thesis: verum

end;

thus A3: PI < (3 / 2) * PI :: thesis: (3 / 2) * PI < 2 * PI

proof

(PI / 2) + (PI / 2) < PI + (PI / 2) by A2, XREAL_1:8;
hence PI < (3 / 2) * PI ; :: thesis: verum

end;

A4: PI + (PI / 2) = (3 / 2) * PI ;
(PI / 2) + ((3 / 2) * PI ) = 2 * PI ;
hence (3 / 2) * PI < 2 * PI by A3, A4, XREAL_1:8; :: thesis: verum