let th be real number ; :: thesis: ( th in ].0,(PI / 2).[ implies cos . th > 0 )
assume that
A1: th in ].0,(PI / 2).[ and
A2: cos . th <= 0 ; :: thesis: contradiction
cos | REAL is continuous by Th72, FDIFF_1:25;
then A3: cos | [.0,th.] is continuous by FCONT_1:16;
A4: 0 < th by A1, XXREAL_1:4;
A5: th is Real by XREAL_0:def 1;
( [.(cos . 0),(cos . th).] \/ [.(cos . th),(cos . 0).] = [.(cos . th),(cos . 0).] & 0 in [.(cos . th),(cos . 0).] ) by A2, Th33, XXREAL_1:1, XXREAL_1:222;
then ex th2 being Real st
( th2 in [.0,th.] & cos . th2 = 0 ) by A3, A4, A5, Th27, FCONT_2:15;
then consider th2 being Real such that
A6: th2 in [.0,th.] and
0 < th and
A7: cos . th2 = 0 by A4;
A8: 0 <= th2 by A6, XXREAL_1:1;
A9: th2 <= th by A6, XXREAL_1:1;
A10: th < PI / 2 by A1, XXREAL_1:4;
A11: 0 < th2 by A7, A8, Th33;
th2 < PI / 2 by A9, A10, XXREAL_0:2;
then A12: th2 / 2 < (PI / 2) / 2 by XREAL_1:74;
PI in ].0,4.[ by Def32;
then PI < 4 by XXREAL_1:4;
then PI / 4 < 4 / 4 by XREAL_1:74;
then A13: th2 / 2 < 1 by A12, XXREAL_0:2;
0 = cos . ((th2 / 2) + (th2 / 2)) by A7
.= ((cos . (th2 / 2)) ^2) - ((sin . (th2 / 2)) * (sin . (th2 / 2))) by Th79
.= ((cos . (th2 / 2)) - (sin . (th2 / 2))) * ((cos . (th2 / 2)) + (sin . (th2 / 2))) ;
then A14: ( (cos . (th2 / 2)) - (sin . (th2 / 2)) = 0 or (cos . (th2 / 2)) + (sin . (th2 / 2)) = 0 ) ;
A15: th2 / 2 in ].0,1.[ by A11, A13, XXREAL_1:4;
].0,1.[ c= [.0,1.] by XXREAL_1:25;
then A16: ( cos . (th2 / 2) > 0 & sin . (th2 / 2) >= - 0 ) by A15, Lm17, Th74;
4 * (th2 / 2) < 4 * 1 by A13, XREAL_1:68;
then A17: 2 * th2 in ].0,4.[ by A11, XXREAL_1:4;
(sin . (th2 / 2)) * ((cos . (th2 / 2)) ") = 1 by A14, A16, XCMPLX_0:def 7;
then tan . ((2 * th2) / 4) = 1 by A15, Th75, RFUNCT_1:def 1;
then 2 * th2 = PI by A17, Def32;
hence contradiction by A1, A9, XXREAL_1:4; :: thesis: verum