let x be Real; :: thesis: for n being Element of NAT holds cos (x + (((2 * n) + 1) * PI)) = - (cos x)
let n be Element of NAT ; :: thesis: cos (x + (((2 * n) + 1) * PI)) = - (cos x)
defpred S₁[ Nat] means cos (x + (((2 * $1) + 1) * PI)) = - (cos x);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: cos (x + (((2 * n) + 1) * PI)) = - (cos x) ; :: thesis: S₁[n + 1]
cos (x + (((2 * (n + 1)) + 1) * PI)) = cos ((x + (((2 * n) + 1) * PI)) + (2 * PI))
.= ((cos (x + (((2 * n) + 1) * PI))) * (cos (2 * PI))) - ((sin (x + (((2 * n) + 1) * PI))) * (sin (2 * PI))) by SIN_COS:75
.= - (cos x) by A2, SIN_COS:77 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ] by SIN_COS:79;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence cos (x + (((2 * n) + 1) * PI)) = - (cos x) ; :: thesis: verum