Theorem cosper

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

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

Proof

Step	Hyp	Ref	Expression
1		cosval	$$⊢A\in ℂ\to \cos A=\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}$$
2		cosval	$$⊢A+K2\mathrm{\pi }\in ℂ\to \cos \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}$$
3	1 2	sinperlem	$$⊢\left(A\in ℂ\wedge K\in \mathbb{Z}\right)\to \cos \left(A+K2\mathrm{\pi }\right)=\cos A$$