Theorem sinper

Description: The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

	Ref	Expression
Assertion	sinper	$$⊢\left(A\in ℂ\wedge K\in \mathbb{Z}\right)\to \sin \left(A+K2\mathrm{\pi }\right)=\sin A$$

Proof

Step	Hyp	Ref	Expression
1		sinval	$$⊢A\in ℂ\to \sin A=\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2\mathrm{i}}$$
2		sinval	$$⊢A+K2\mathrm{\pi }\in ℂ\to \sin \left(A+K2\mathrm{\pi }\right)=\frac{{\mathrm{e}}^{\mathrm{i}\left(A+K2\mathrm{\pi }\right)}-{\mathrm{e}}^{\left(-\mathrm{i}\right)\left(A+K2\mathrm{\pi }\right)}}{2\mathrm{i}}$$
3	1 2	sinperlem	$$⊢\left(A\in ℂ\wedge K\in \mathbb{Z}\right)\to \sin \left(A+K2\mathrm{\pi }\right)=\sin A$$