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