let r be Real; :: thesis: for i being Integer holds sin r = sin (((2 * PI) * i) + r)
let i be Integer; :: thesis: sin r = sin (((2 * PI) * i) + r)
A1: sin . r = sin r by SIN_COS:def 17;
A2: sin . (((2 * PI) * i) + r) = sin (((2 * PI) * i) + r) by SIN_COS:def 17;
A3: sin . (((2 * PI) * (- i)) + (((2 * PI) * i) + r)) = sin (((2 * PI) * (- i)) + (((2 * PI) * i) + r)) by SIN_COS:def 17;
per cases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; :: thesis: sin r = sin (((2 * PI) * i) + r)
then reconsider iN = i as Element of NAT by INT_1:3;
sin r = sin (((2 * PI) * iN) + r) by A1, A2, SIN_COS2:10;
hence sin r = sin (((2 * PI) * i) + r) ; :: thesis: verum
end;
suppose i < 0 ; :: thesis: sin r = sin (((2 * PI) * i) + r)
then reconsider iN = - i as Element of NAT by INT_1:3;
set aa = ((2 * PI) * i) + r;
sin (((2 * PI) * i) + r) = sin (((2 * PI) * iN) + (((2 * PI) * i) + r)) by A2, A3, SIN_COS2:10;
hence sin r = sin (((2 * PI) * i) + r) ; :: thesis: verum
end;
end;