Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

For −1<y<1, (arcsin⁡y)′=1/1−y2 and (arccos⁡y)′=−1/1−y2

Statement

For −1<y<1,

(arcsin⁡y)′=11−y2,(arccos⁡y)′=−11−y2.

Facts & Assumptions

Given: A real number y with −1<y<1.

[L1]

Principal inverse sine and cosine are the inverses of the indicated restricted functions (Principal inverse sine and inverse cosine).

[L2]

Sine and cosine are differentiable, hence continuous, with derivatives cos⁡ and −sin⁡ (The derivatives of sine and cosine are cosine and minus sine, A function differentiable at c is continuous at c).

[L3]

Sine is strictly increasing on [−π/2,π/2] and strictly decreasing on [π/2,3π/2], while cosine is strictly decreasing on [0,π]; the special values are sin⁡0=sin⁡π=0 and cos⁡(π/2)=0, and cosine is even (Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi, Parity and the Pythagorean identity for sine and cosine).

[L4]

sin⁡2t+cos⁡2t=1 for every t (Parity and the Pythagorean identity for sine and cosine).

[L5]

Every nonnegative real has a unique nonnegative square root (Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}).

[L6]

The inverse of a continuous injective function on a nondegenerate interval has derivative the reciprocal of the original derivative wherever that derivative is nonzero (Derivative of an inverse: if f is continuous and injective on a nondegenerate interval I and differentiable at c∈I with f′(c)≠0, then the inverse g is differentiable at f(c) with g′(f(c))=1/f′(c); and if f′(c)=0 then g is not differentiable at f(c)).

Proof

technique · direct
1.1

Put a:=arcsin⁡y and b:=arccos⁡y. Then sin⁡a=y, cos⁡b=y, and a,b lie in the interiors of their respective principal intervals.

L1given
2.1

The interval placement of step 1.1, the monotonicity and special values in [L3], and evenness of cosine give cos⁡a>0 and sin⁡b>0. The Pythagorean identity then gives cos⁡a=1−y2 and sin⁡b=1−y2.

step 1.1L3L4L5
3.1

Apply [L6] to sine on [−π/2,π/2] at a: [L1] supplies injectivity and [L2] supplies continuity. Since its derivative there is cos⁡a≠0, the inverse is differentiable at y with (arcsin⁡y)′=1/cos⁡a=1/1−y2.

step 1.1step 2.1L1L2L6
3.2

Apply [L6] to cosine on [0,π] at b: [L1] supplies injectivity and [L2] supplies continuity. Its derivative is −sin⁡b≠0, so (arccos⁡y)′=−1/sin⁡b=−1/1−y2.

step 1.1step 2.1L1L2L6
4.1

Steps 3.1 and 3.2 prove the two derivative formulas.

step 3.1step 3.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources