Sine is 2π-periodic

Statement

For every real $x$, $$\sin(x + 2\pi) = \sin x, \qquad \cos(x + 2\pi) = \cos x.$$ The number $2\pi$ is the smallest positive period of $\sin$ and of $\cos$.

Remarks

From $\cos \pi = -1$ and $\sin \pi = 0$, the addition formulas give $\cos 2\pi = 1$ and $\sin 2\pi = 0$. Apply the addition formulas again with $y = 2\pi$. So $\sin$ and $\cos$ are periodic functions. Also $\sin(x + \pi) = -\sin x$ and $\sin(x + \pi/2) = \cos x$. Mathlib states the periodicity as Real.sin_periodic.

Explanations

L1 human

A full turn around the unit circle has length $2\pi$, and it brings the point back to where it started. So the graphs of sine and cosine repeat after each interval of length $2\pi$.