let a, b be Real; :: thesis: for i being non zero Integer holds b + (a (#) sin) is (2 * PI) * i -periodic

let i be non zero Integer; :: thesis: b + (a (#) sin) 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;

let i be non zero Integer; :: thesis: b + (a (#) sin) 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;

end;

suppose
i = k
; :: thesis: b + (a (#) sin) is (2 * PI) * i -periodic

then
ex m being Nat st i = m + 1
by NAT_1:6;

hence b + (a (#) sin) is (2 * PI) * i -periodic by Lm28; :: thesis: verum

end;hence b + (a (#) sin) is (2 * PI) * i -periodic by Lm28; :: thesis: verum

suppose A2:
i = - k
; :: thesis: b + (a (#) sin) is (2 * PI) * i -periodic

then consider m being Nat such that

A3: - i = m + 1 by NAT_1:6;

b + (a (#) sin) is (2 * PI) * (m + 1) -periodic by Lm28;

then b + (a (#) sin) is - ((2 * PI) * (m + 1)) -periodic by Th14;

hence b + (a (#) sin) is (2 * PI) * i -periodic by A2, A3; :: thesis: verum

end;A3: - i = m + 1 by NAT_1:6;

b + (a (#) sin) is (2 * PI) * (m + 1) -periodic by Lm28;

then b + (a (#) sin) is - ((2 * PI) * (m + 1)) -periodic by Th14;

hence b + (a (#) sin) is (2 * PI) * i -periodic by A2, A3; :: thesis: verum