Derivative of sine

Statement

The sine function is differentiable on $\mathbb{R}$, and $\sin'(x) = \cos x$ for all real $x$.

Remarks

Differentiate the power series term by term. The derivative of $\frac{(-1)^n x^{2n+1}}{(2n+1)!}$ is $\frac{(-1)^n x^{2n}}{(2n)!}$, the term of the cosine series. With the addition formula, the claim reduces to the limits $\frac{\sin h}{h} \to 1$ and $\frac{\cos h - 1}{h} \to 0$. Mathlib states it as Real.hasDerivAt_sin.

Explanations

L1 human

The slope of the sine curve at $x$ is $\cos x$. At $x = 0$ the sine curve rises with slope $1$, and at $x = \pi/2$ it is flat.