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
A3: cos | REAL is continuous by Th72, FDIFF_1:33;
A4: cos | [.0 ,th.] is continuous by A3, FCONT_1:17;
A5: 0 < th by A1, XXREAL_1:4;
A6: th is Real by XREAL_0:def 1;
A7: ( [.(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;
A8: ex th2 being Real st
( th2 in [.0 ,th.] & cos . th2 = 0 ) by A4, A5, A6, A7, Th27, FCONT_2:16;
consider th2 being Real such that
A9: th2 in [.0 ,th.] and
0 < th and
A10: cos . th2 = 0 by A5, A8;
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;
A15: th2 < PI / 2 by A12, A13, XXREAL_0:2;
A16: th2 / 2 < (PI / 2) / 2 by A15, XREAL_1:76;
A17: PI in ].0 ,4.[ by Def32;
A18: PI < 4 by A17, XXREAL_1:4;
A19: PI / 4 < 4 / 4 by A18, XREAL_1:76;
A20: th2 / 2 < 1 by A16, A19, XXREAL_0:2;
A21: 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))) ;
A22: ( (cos . (th2 / 2)) - (sin . (th2 / 2)) = 0 or (cos . (th2 / 2)) + (sin . (th2 / 2)) = 0 ) by A21;
A23: th2 / 2 in ].0 ,1.[ by A14, A20, XXREAL_1:4;
A24: ].0 ,1.[ c= [.0 ,1.] by XXREAL_1:25;
A25: ( cos . (th2 / 2) > 0 & sin . (th2 / 2) >= - 0 ) by A23, A24, Lm18, Th74;
A26: 4 * (th2 / 2) < 4 * 1 by A20, XREAL_1:70;
A27: 2 * th2 in ].0 ,4.[ by A14, A26, XXREAL_1:4;
A28: (sin . (th2 / 2)) * ((cos . (th2 / 2)) " ) = 1 by A22, A25, XCMPLX_0:def 7;
A29: tan . ((2 * th2) / 4) = 1 by A23, A28, Th75, RFUNCT_1:def 4;
A30: 2 * th2 = PI by A27, A29, Def32;
thus contradiction by A1, A12, A30, XXREAL_1:4; :: thesis: verum