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