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:33;
then A4: cos | [.0 ,th.] is continuous by FCONT_1:17;
A5: 0 < th by A1, XXREAL_1:4;
A6: 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 A4, A5, A6, Th27, FCONT_2:16;
then consider th2 being Real such that
A9: th2 in [.0 ,th.] and
0 < th and
A10: cos . th2 = 0 by A5;
A11: 0 <= th2 by A9, XXREAL_1:1;
A12: th2 <= th by A9, XXREAL_1:1;
A13: th < PI / 2 by A1, XXREAL_1:4;
A14: 0 < th2 by A10, A11, Th33;
th2 < PI / 2 by A12, A13, XXREAL_0:2;
then A16: th2 / 2 < (PI / 2) / 2 by XREAL_1:76;
PI in ].0 ,4.[ by Def32;
then PI < 4 by XXREAL_1:4;
then PI / 4 < 4 / 4 by XREAL_1:76;
then A20: th2 / 2 < 1 by A16, XXREAL_0:2;
0 = cos . ((th2 / 2) + (th2 / 2)) by A10
.= ((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 A22: ( (cos . (th2 / 2)) - (sin . (th2 / 2)) = 0 or (cos . (th2 / 2)) + (sin . (th2 / 2)) = 0 ) ;
A23: th2 / 2 in ].0 ,1.[ by A14, A20, XXREAL_1:4;
].0 ,1.[ c= [.0 ,1.] by XXREAL_1:25;
then A25: ( cos . (th2 / 2) > 0 & sin . (th2 / 2) >= - 0 ) by A23, Lm18, Th74;
4 * (th2 / 2) < 4 * 1 by A20, XREAL_1:70;
then A27: 2 * th2 in ].0 ,4.[ by A14, XXREAL_1:4;
(sin . (th2 / 2)) * ((cos . (th2 / 2)) " ) = 1 by A22, A25, XCMPLX_0:def 7;
then tan . ((2 * th2) / 4) = 1 by A23, Th75, RFUNCT_1:def 4;
then 2 * th2 = PI by A27, Def32;
hence contradiction by A1, A12, XXREAL_1:4; :: thesis: verum