Derivative of arcsine

Statement

The arcsine is differentiable on $(-1, 1)$, and $$\frac{d}{dx} \arcsin x = \frac{1}{\sqrt{1 - x^2}} \quad \text{for } -1 < x < 1.$$

Remarks

Let $y = \arcsin x$. The inverse function rule gives the derivative $\frac{1}{\cos y}$. By the Pythagorean identity, $\cos y = \sqrt{1 - x^2}$, since $\cos y > 0$ for $|y| < \pi/2$. The arcsine is not differentiable at $\pm 1$. Its graph has vertical tangents there. Similarly, $\frac{d}{dx} \arccos x = -\frac{1}{\sqrt{1 - x^2}}$. Mathlib states the main claim as Real.hasDerivAt_arcsin.

Explanations

L1 human

The derivative of the arcsine is an algebraic function, although the arcsine itself is not. It becomes infinite at the ends of the interval $[-1, 1]$.