let i be Integer; sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing
defpred S1[ Integer] means sin | [.((- (PI / 2)) + H1($1)),((PI / 2) + H1($1)).] is increasing ;
A1:
for i being Integer st S1[i] holds
( S1[i - 1] & S1[i + 1] )
proof
let i be
Integer;
( S1[i] implies ( S1[i - 1] & S1[i + 1] ) )
assume A2:
S1[
i]
;
( S1[i - 1] & S1[i + 1] )
set Z =
[.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).];
thus
S1[
i - 1]
S1[i + 1]proof
set Y =
[.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).];
now for r1, r2 being Real st r1 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) & r2 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) & r1 < r2 holds
sin . r1 < sin . r2let r1,
r2 be
Real;
( r1 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) & r2 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) & r1 < r2 implies sin . r1 < sin . r2 )assume
(
r1 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) &
r2 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) )
;
( r1 < r2 implies sin . r1 < sin . r2 )then A3:
(
r1 + (2 * PI) in [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] /\ (dom sin) &
r2 + (2 * PI) in [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] /\ (dom sin) )
by Lm12, SIN_COS:24;
assume
r1 < r2
;
sin . r1 < sin . r2then
r1 + (2 * PI) < r2 + (2 * PI)
by XREAL_1:6;
then
sin . (r1 + (2 * PI)) < sin . (r2 + ((2 * PI) * 1))
by A2, A3, RFUNCT_2:20;
then
sin . (r1 + ((2 * PI) * 1)) < sin . r2
by Th8;
hence
sin . r1 < sin . r2
by Th8;
verum end;
hence
S1[
i - 1]
by RFUNCT_2:20;
verum
end;
set Y =
[.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).];
A4:
[.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] = [.((- (PI / 2)) + H1((i + 1) - 1)),((PI / 2) + H1((i + 1) - 1)).]
;
now for r1, r2 being Real st r1 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) & r2 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) & r1 < r2 holds
sin . r1 < sin . r2let r1,
r2 be
Real;
( r1 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) & r2 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) & r1 < r2 implies sin . r1 < sin . r2 )assume
(
r1 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) &
r2 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) )
;
( r1 < r2 implies sin . r1 < sin . r2 )then A5:
(
r1 - (2 * PI) in [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] /\ (dom sin) &
r2 - (2 * PI) in [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] /\ (dom sin) )
by A4, Lm14, SIN_COS:24;
assume
r1 < r2
;
sin . r1 < sin . r2then
r1 - (2 * PI) < r2 - (2 * PI)
by XREAL_1:9;
then
sin . (r1 - (2 * PI)) < sin . (r2 + ((2 * PI) * (- 1)))
by A2, A5, RFUNCT_2:20;
then
sin . (r1 + ((2 * PI) * (- 1))) < sin . r2
by Th8;
hence
sin . r1 < sin . r2
by Th8;
verum end;
hence
S1[
i + 1]
by RFUNCT_2:20;
verum
end;
A6:
S1[ 0 ]
by COMPTRIG:23;
for i being Integer holds S1[i]
from INT_1:sch 4(A6, A1);
hence
sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing
; verum