let th be Real; :: thesis: ( th in [.0,1.] implies sin . th >= 0 )
assume A1: th in [.0,1.] ; :: thesis: sin . th >= 0
then A2: th <= 1 by XXREAL_1:1;
sin . th >= sin . 0
proof
now :: thesis: sin . th >= sin . 0
per cases ( th = 0 or 0 < th ) by A1, XXREAL_1:1;
suppose A3: 0 < th ; :: thesis: sin . th >= sin . 0
sin | REAL is continuous by Th67, FDIFF_1:25;
then sin | [.0,th.] is continuous by FCONT_1:16;
then consider r being Real such that
A4: r in ].0,th.[ and
A5: diff (sin,r) = ((sin . th) - (sin . 0)) / (th - 0) by A3, Th24, Th67, FDIFF_1:26, ROLLE:3;
A6: r < th by A4, XXREAL_1:4;
A7: 0 < r by A4, XXREAL_1:4;
r < 1 by A2, A6, XXREAL_0:2;
then r in [.0,1.] by A7, XXREAL_1:1;
then cos . r > 0 by Th68;
then (sin . th) - (sin . 0) > 0 by A3, A5, Th67;
hence sin . th >= sin . 0 by XREAL_1:47; :: thesis: verum
end;
end;
end;
hence sin . th >= sin . 0 ; :: thesis: verum
end;
hence sin . th >= 0 by Th30; :: thesis: verum