Metamath Proof Explorer


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 A K cos A + K 2 π = cos A

Proof

Step Hyp Ref Expression
1 cosval A cos A = e i A + e i A 2
2 cosval A + K 2 π cos A + K 2 π = e i A + K 2 π + e i A + K 2 π 2
3 1 2 sinperlem A K cos A + K 2 π = cos A