let i be Integer; :: thesis: cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing
defpred S₁[ Integer] means cos | [.(PI + H₁($1)),((2 * PI) + H₁($1)).] is increasing ;
A1: for i being Integer st S₁[i] holds
( S₁[i - 1] & S₁[i + 1] )

proof

let i be Integer; :: thesis: ( S₁[i] implies ( S₁[i - 1] & S₁[i + 1] ) )
assume A2: S₁[i] ; :: thesis: ( S₁[i - 1] & S₁[i + 1] )
set Z = [.(PI + H₁((i - 1) + 1)),((2 * PI) + H₁((i - 1) + 1)).];
thus S₁[i - 1] :: thesis: S₁[i + 1]

proof

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

now :: thesis: for r1, r2 being Real st r1 in [.(PI + H₁(i - 1)),((2 * PI) + H₁(i - 1)).] /\ (dom cos) & r2 in [.(PI + H₁(i - 1)),((2 * PI) + H₁(i - 1)).] /\ (dom cos) & r1 < r2 holds
cos . r1 < cos . r2

let r1, r2 be Real; :: thesis: ( r1 in [.(PI + H₁(i - 1)),((2 * PI) + H₁(i - 1)).] /\ (dom cos) & r2 in [.(PI + H₁(i - 1)),((2 * PI) + H₁(i - 1)).] /\ (dom cos) & r1 < r2 implies cos . r1 < cos . r2 )
assume ( r1 in [.(PI + H₁(i - 1)),((2 * PI) + H₁(i - 1)).] /\ (dom cos) & r2 in [.(PI + H₁(i - 1)),((2 * PI) + H₁(i - 1)).] /\ (dom cos) ) ; :: thesis: ( r1 < r2 implies cos . r1 < cos . r2 )
then A3: ( r1 + (2 * PI) in [.(PI + H₁((i - 1) + 1)),((2 * PI) + H₁((i - 1) + 1)).] /\ (dom cos) & r2 + (2 * PI) in [.(PI + H₁((i - 1) + 1)),((2 * PI) + H₁((i - 1) + 1)).] /\ (dom cos) ) by Lm12, SIN_COS:24;
assume r1 < r2 ; :: thesis: cos . r1 < cos . r2
then r1 + (2 * PI) < r2 + (2 * PI) by XREAL_1:6;
then cos . (r1 + (2 * PI)) < cos . (r2 + ((2 * PI) * 1)) by A2, A3, RFUNCT_2:20;
then cos . (r1 + ((2 * PI) * 1)) < cos . r2 by Th10;
hence cos . r1 < cos . r2 by Th10; :: thesis: verum

end;

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

end;

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

now :: thesis: for r1, r2 being Real st r1 in [.(PI + H₁(i + 1)),((2 * PI) + H₁(i + 1)).] /\ (dom cos) & r2 in [.(PI + H₁(i + 1)),((2 * PI) + H₁(i + 1)).] /\ (dom cos) & r1 < r2 holds
cos . r1 < cos . r2

let r1, r2 be Real; :: thesis: ( r1 in [.(PI + H₁(i + 1)),((2 * PI) + H₁(i + 1)).] /\ (dom cos) & r2 in [.(PI + H₁(i + 1)),((2 * PI) + H₁(i + 1)).] /\ (dom cos) & r1 < r2 implies cos . r1 < cos . r2 )
assume ( r1 in [.(PI + H₁(i + 1)),((2 * PI) + H₁(i + 1)).] /\ (dom cos) & r2 in [.(PI + H₁(i + 1)),((2 * PI) + H₁(i + 1)).] /\ (dom cos) ) ; :: thesis: ( r1 < r2 implies cos . r1 < cos . r2 )
then A5: ( r1 - (2 * PI) in [.(PI + H₁((i - 1) + 1)),((2 * PI) + H₁((i - 1) + 1)).] /\ (dom cos) & r2 - (2 * PI) in [.(PI + H₁((i - 1) + 1)),((2 * PI) + H₁((i - 1) + 1)).] /\ (dom cos) ) by A4, Lm14, SIN_COS:24;
assume r1 < r2 ; :: thesis: cos . r1 < cos . r2
then r1 - (2 * PI) < r2 - (2 * PI) by XREAL_1:9;
then cos . (r1 - (2 * PI)) < cos . (r2 + ((2 * PI) * (- 1))) by A2, A5, RFUNCT_2:20;
then cos . (r1 + ((2 * PI) * (- 1))) < cos . r2 by Th10;
hence cos . r1 < cos . r2 by Th10; :: thesis: verum

end;

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

end;

A6: S₁[ 0 ] by COMPTRIG:26;
for i being Integer holds S₁[i] from INT_1:sch 4(A6, A1);
hence cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing ; :: thesis: verum