now for r1, r2 being Real st r1 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r2 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r1 < r2 holds
sin . r2 > sin . r1let r1,
r2 be
Real;
( r1 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r2 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r1 < r2 implies sin . r2 > sin . r1 )assume that A1:
r1 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin)
and A2:
r2 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin)
and A3:
r1 < r2
;
sin . r2 > sin . r1A4:
r1 in dom sin
by A1, XBOOLE_0:def 4;
set r3 =
(r1 + r2) / 2;
r1 in [.(- (PI / 2)),(PI / 2).]
by A1, XBOOLE_0:def 4;
then A5:
- (PI / 2) <= r1
by XXREAL_1:1;
|.(sin ((r1 + r2) / 2)).| <= 1
by SIN_COS:27;
then A6:
|.(sin . ((r1 + r2) / 2)).| <= 1
by SIN_COS:def 17;
then A7:
sin . ((r1 + r2) / 2) <= 1
by ABSVALUE:5;
r2 in [.(- (PI / 2)),(PI / 2).]
by A2, XBOOLE_0:def 4;
then A8:
r2 <= PI / 2
by XXREAL_1:1;
A9:
r1 < (r1 + r2) / 2
by A3, XREAL_1:226;
then A10:
- (PI / 2) < (r1 + r2) / 2
by A5, XXREAL_0:2;
A11:
(r1 + r2) / 2
< r2
by A3, XREAL_1:226;
then
(r1 + r2) / 2
< PI / 2
by A8, XXREAL_0:2;
then
(r1 + r2) / 2
in ].(- (PI / 2)),(PI / 2).[
by A10, XXREAL_1:4;
then A12:
(r1 + r2) / 2
in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin)
by SIN_COS:24, XBOOLE_0:def 4;
|.(sin r2).| <= 1
by SIN_COS:27;
then
|.(sin . r2).| <= 1
by SIN_COS:def 17;
then A13:
sin . r2 >= - 1
by ABSVALUE:5;
A14:
r2 in dom sin
by A2, XBOOLE_0:def 4;
A15:
sin . ((r1 + r2) / 2) >= - 1
by A6, ABSVALUE:5;
now sin . r2 > sin . r1per cases
( - (PI / 2) < r1 or - (PI / 2) = r1 )
by A5, XXREAL_0:1;
suppose A16:
- (PI / 2) < r1
;
sin . r2 > sin . r1then A17:
- (PI / 2) < r2
by A3, XXREAL_0:2;
now sin . r2 > sin . r1per cases
( r2 < PI / 2 or r2 = PI / 2 )
by A8, XXREAL_0:1;
suppose A18:
r2 < PI / 2
;
sin . r2 > sin . r1then
r1 < PI / 2
by A3, XXREAL_0:2;
then
r1 in ].(- (PI / 2)),(PI / 2).[
by A16, XXREAL_1:4;
then A19:
r1 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin)
by A4, XBOOLE_0:def 4;
r2 in ].(- (PI / 2)),(PI / 2).[
by A17, A18, XXREAL_1:4;
then
r2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin)
by A14, XBOOLE_0:def 4;
hence
sin . r2 > sin . r1
by A3, A19, Th19, RFUNCT_2:20;
verum end; suppose A20:
r2 = PI / 2
;
not sin . r2 <= sin . r1then
r1 in ].(- (PI / 2)),(PI / 2).[
by A3, A16, XXREAL_1:4;
then
r1 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin)
by A4, XBOOLE_0:def 4;
then A21:
sin . ((r1 + r2) / 2) > sin . r1
by A9, A12, Th19, RFUNCT_2:20;
assume
sin . r2 <= sin . r1
;
contradictionhence
contradiction
by A7, A20, A21, SIN_COS:76, XXREAL_0:2;
verum end; end; end; hence
sin . r2 > sin . r1
;
verum end; suppose A22:
- (PI / 2) = r1
;
sin . r2 > sin . r1now not sin . r2 <= sin . r1per cases
( r2 < PI / 2 or r2 = PI / 2 )
by A8, XXREAL_0:1;
suppose
r2 < PI / 2
;
not sin . r2 <= sin . r1then
r2 in ].(- (PI / 2)),(PI / 2).[
by A3, A22, XXREAL_1:4;
then
r2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin)
by A14, XBOOLE_0:def 4;
then A23:
sin . r2 > sin . ((r1 + r2) / 2)
by A11, A12, Th19, RFUNCT_2:20;
assume
sin . r2 <= sin . r1
;
contradictionthen
sin . r2 <= - 1
by A22, SIN_COS:30, SIN_COS:76;
hence
contradiction
by A15, A13, A23, XXREAL_0:1;
verum end; end; end; hence
sin . r2 > sin . r1
;
verum end; end; end; hence
sin . r2 > sin . r1
;
verum end;
hence
sin | [.(- (PI / 2)),(PI / 2).] is increasing
by RFUNCT_2:20; verum