let i be non zero Integer; :: thesis: cos is (2 * PI) * i -periodic
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: ( i = k or i = - k ) by INT_1:def 1;
per cases ( i = k or i = - k ) by A1;
suppose i = k ; :: thesis: cos is (2 * PI) * i -periodic
then ex m being Nat st i = m + 1 by NAT_1:6;
hence cos is (2 * PI) * i -periodic by Lm5; :: thesis: verum
end;
suppose A2: i = - k ; :: thesis: cos is (2 * PI) * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
cos is (2 * PI) * (m + 1) -periodic by Lm5;
then cos is - ((2 * PI) * (m + 1)) -periodic by Th14;
hence cos is (2 * PI) * i -periodic by A2, A3; :: thesis: verum
end;
end;