let i be integer number ; :: thesis: sin | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).] is increasing
defpred S₁[ Integer] means sin | [.((- (PI / 2)) + H₁($1)),((PI / 2) + H₁($1)).] is increasing ;
A1: S₁[ 0 ] by COMPTRIG:39;
A2: for i being integer number st S₁[i] holds
( S₁[i - 1] & S₁[i + 1] )

proof

let i be integer number ; :: thesis: ( S₁[i] implies ( S₁[i - 1] & S₁[i + 1] ) )
assume A3: S₁[i] ; :: thesis: ( S₁[i - 1] & S₁[i + 1] )
set Z = [.((- (PI / 2)) + H₁((i - 1) + 1)),((PI / 2) + H₁((i - 1) + 1)).];
thus S₁[i - 1] :: thesis: S₁[i + 1]

proof

set Y = [.((- (PI / 2)) + H₁(i - 1)),((PI / 2) + H₁(i - 1)).];

now

let r1, r2 be Element of REAL ; :: thesis: ( r1 in [.((- (PI / 2)) + H₁(i - 1)),((PI / 2) + H₁(i - 1)).] /\ (dom sin ) & r2 in [.((- (PI / 2)) + H₁(i - 1)),((PI / 2) + H₁(i - 1)).] /\ (dom sin ) & r1 < r2 implies sin . r1 < sin . r2 )
assume ( r1 in [.((- (PI / 2)) + H₁(i - 1)),((PI / 2) + H₁(i - 1)).] /\ (dom sin ) & r2 in [.((- (PI / 2)) + H₁(i - 1)),((PI / 2) + H₁(i - 1)).] /\ (dom sin ) ) ; :: thesis: ( r1 < r2 implies sin . r1 < sin . r2 )
then A4: ( r1 + (2 * PI ) in [.((- (PI / 2)) + H₁((i - 1) + 1)),((PI / 2) + H₁((i - 1) + 1)).] /\ (dom sin ) & r2 + (2 * PI ) in [.((- (PI / 2)) + H₁((i - 1) + 1)),((PI / 2) + H₁((i - 1) + 1)).] /\ (dom sin ) ) by Lm1, Lm25;
assume r1 < r2 ; :: thesis: sin . r1 < sin . r2
then r1 + (2 * PI ) < r2 + (2 * PI ) by XREAL_1:8;
then sin . (r1 + (2 * PI )) < sin . (r2 + ((2 * PI ) * 1)) by A3, A4, RFUNCT_2:43;
then sin . (r1 + ((2 * PI ) * 1)) < sin . r2 by Th8;
hence sin . r1 < sin . r2 by Th8; :: thesis: verum

end;

hence S₁[i - 1] by RFUNCT_2:43; :: thesis: verum

end;

set Y = [.((- (PI / 2)) + H₁(i + 1)),((PI / 2) + H₁(i + 1)).];
A5: [.((- (PI / 2)) + H₁((i - 1) + 1)),((PI / 2) + H₁((i - 1) + 1)).] = [.((- (PI / 2)) + H₁((i + 1) - 1)),((PI / 2) + H₁((i + 1) - 1)).] ;

now

let r1, r2 be Element of REAL ; :: thesis: ( r1 in [.((- (PI / 2)) + H₁(i + 1)),((PI / 2) + H₁(i + 1)).] /\ (dom sin ) & r2 in [.((- (PI / 2)) + H₁(i + 1)),((PI / 2) + H₁(i + 1)).] /\ (dom sin ) & r1 < r2 implies sin . r1 < sin . r2 )
assume ( r1 in [.((- (PI / 2)) + H₁(i + 1)),((PI / 2) + H₁(i + 1)).] /\ (dom sin ) & r2 in [.((- (PI / 2)) + H₁(i + 1)),((PI / 2) + H₁(i + 1)).] /\ (dom sin ) ) ; :: thesis: ( r1 < r2 implies sin . r1 < sin . r2 )
then A6: ( r1 - (2 * PI ) in [.((- (PI / 2)) + H₁((i - 1) + 1)),((PI / 2) + H₁((i - 1) + 1)).] /\ (dom sin ) & r2 - (2 * PI ) in [.((- (PI / 2)) + H₁((i - 1) + 1)),((PI / 2) + H₁((i - 1) + 1)).] /\ (dom sin ) ) by A5, Lm1, Lm27;
assume r1 < r2 ; :: thesis: sin . r1 < sin . r2
then r1 - (2 * PI ) < r2 - (2 * PI ) by XREAL_1:11;
then sin . (r1 - (2 * PI )) < sin . (r2 + ((2 * PI ) * (- 1))) by A3, A6, RFUNCT_2:43;
then sin . (r1 + ((2 * PI ) * (- 1))) < sin . r2 by Th8;
hence sin . r1 < sin . r2 by Th8; :: thesis: verum

end;

hence S₁[i + 1] by RFUNCT_2:43; :: thesis: verum

end;

for i being integer number holds S₁[i] from INT_1:sch 4(A1, A2);
hence sin | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).] is increasing ; :: thesis: verum