Session-authored (Fable 5 assisted)

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.

✓ 3 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Further Trigonometric Identities and Inverse Functions

1 · Prerequisites

2 · Summary

The earlier trigonometric development supplies sine, cosine, tangent, their addition formulas, signs, periods, monotonicity, and derivatives. The preceding treatment of monotone functions and continuous inverses supplies the analytic criterion needed to choose and control principal inverse branches.

This core defines the principal inverse sine, cosine, and tangent branches and proves their interior derivative formulae. For principal arctangent it also derives the oriented-integral representation, its power series on $|x|<1$ , and the Gregory--Leibniz endpoint value. Principal ranges and endpoint restrictions remain explicit throughout.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03Open item page →

Principal inverse sine and inverse cosine

Definition

Sine is differentiable, hence continuous, and strictly increasing on $[-\pi/2,\pi/2]$ ; its endpoint values are $-1$ and $1$ (The derivatives of sine and cosine are cosine and minus sine, A function differentiable at $c$ is continuous at $c$ , 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). The intermediate value theorem therefore makes its restricted image exactly $[-1,1]$ (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$ ). Likewise, cosine is continuous and strictly decreasing on $[0,\pi]$ , with endpoint values $1$ and $-1$ , so its restricted image is $[-1,1]$ (Signs, monotonicity intervals, and ranges of sine and cosine, The derivatives of sine and cosine are cosine and minus sine, A function differentiable at $c$ is continuous at $c$ , Quarter-turn values and shifts by pi/2 and pi, Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$ ). Their principal inverses are denoted

$\arcsin:[-1,1]\to[-\pi/2,\pi/2],\qquad\arccos:[-1,1]\to[0,\pi],$

and are characterised by

$\sin(\arcsin y)=y,\qquad\cos(\arccos y)=y\qquad(-1\le y\le1).$

The chosen target intervals are part of the notation: without them, inverse sine and inverse cosine would be multivalued relations rather than functions. Their continuity follows from Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f[I]$ , and the inverse $g : f[I] \to I$ is continuous and strictly monotone in the same sense as $f$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

For $-1<y<1$ , $(\arcsin y)^{\prime}=1/\sqrt{1-y^2}$ and $(\arccos y)^{\prime}=-1/\sqrt{1-y^2}$

Statement

For $-1<y<1$ ,

$(\arcsin y)'=\frac{1}{\sqrt{1-y^2}},\qquad(\arccos y)'=-\frac{1}{\sqrt{1-y^2}}.$

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 $[-\pi/2,\pi/2]$ and strictly decreasing on $[\pi/2,3\pi/2]$ , while cosine is strictly decreasing on $[0,\pi]$ ; the special values are $\sin0=\sin\pi=0$ and $\cos(\pi/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 $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 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 \in I$ with $f'(c) \ne 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=\sqrt{1-y^2}$ and $\sin b=\sqrt{1-y^2}$ .

step 1.1L3L4L5

3.1

Apply [L6] to sine on $[-\pi/2,\pi/2]$ at $a$ : [L1] supplies injectivity and [L2] supplies continuity. Since its derivative there is $\cos a\ne0$ , the inverse is differentiable at $y$ with $(\arcsin y)'=1/\cos a=1/\sqrt{1-y^2}$ .

step 1.1step 2.1L1L2L6

3.2

Apply [L6] to cosine on $[0,\pi]$ at $b$ : [L1] supplies injectivity and [L2] supplies continuity. Its derivative is $-\sin b\ne0$ , so $(\arccos y)'=-1/\sin b=-1/\sqrt{1-y^2}$ .

step 1.1step 2.1L1L2L6

4.1

Steps 3.1 and 3.2 prove the two derivative formulas.

step 3.1step 3.2∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Tangent is a continuous strictly increasing bijection from $(-\pi/2,\pi/2)$ onto $\mathbb R$

Statement

The restriction

$\tan:(-\pi/2,\pi/2)\longrightarrow\mathbb R$

is continuous, strictly increasing, and bijective.

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Tangent is defined where cosine is nonzero and is differentiable on its natural domain with $(\tan x)'=\sec^2x$ ; differentiability there implies continuity (Tangent, cotangent, secant, and cosecant on their exact natural domains, Derivatives and fundamental periods of tangent, cotangent, secant, and cosecant, A function differentiable at $c$ is continuous at $c$ ).

[L2]

On the natural domain of tangent, $\sec^2x=1+\tan^2x$ ; moreover $\sec x=1/\cos x\ne0$ , so $\sec^2x>0$ (Pythagorean and parity identities for all six trigonometric functions on their natural domains, Tangent, cotangent, secant, and cosecant on their exact natural domains, Squares of nonzero elements are positive).

[L3]

The map $t\mapsto(\cos t,\sin t)$ maps $[0,2\pi)$ bijectively onto the unit circle ( $t\mapsto(\cos t,\sin t)$ is a bijection from $[0,2\pi)$ onto the real unit circle).

[L4]

Cosine decreases on $[0,\pi]$ , increases on $[\pi,2\pi]$ , has zeros at $\pi/2$ and $3\pi/2$ in $[0,2\pi)$ , and sine and cosine have period $2\pi$ (Signs, monotonicity intervals, and ranges of sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi).

[L5]

Every nonnegative real has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ).

[L6]

A continuous function on an interval whose derivative is positive at every interior point is strictly increasing (On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f' \ge 0$ throughout gives $f$ nondecreasing, $f' > 0$ gives $f$ increasing, $f' \le 0$ and $f' < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f' \ge 0$ and a nonincreasing $f$ has $f' \le 0$ wherever it is differentiable, and no strict converse is claimed).

Proof

technique · direct

1.1

By [L4], cosine is positive on $(-\pi/2,\pi/2)$ , so tangent is defined and continuous there. By [L1], [L2], and [L6], its derivative is positive and the restriction is strictly increasing, hence injective.

L1L2L4L6

1.2

Fix $y\in\mathbb R$ and put $c:=\frac1{\sqrt{1+y^2}},\qquad s:=\frac y{\sqrt{1+y^2}}.$ The radicand is positive, $c>0$ , and $c^2+s^2=1$ . Thus [L3] supplies a unique $t\in[0,2\pi)$ with $(\cos t,\sin t)=(c,s)$ .

L3L5algebra

2.1

Since $\cos t=c>0$ , [L4] places $t$ in $[0,\pi/2)\cup(3\pi/2,2\pi)$ . Set $u:=t$ in the first case and $u:=t-2\pi$ in the second. Then $u\in(-\pi/2,\pi/2)$ and periodicity of sine and cosine gives $\tan u=s/c=y$ . Hence the restriction is surjective.

step 1.2L1L4

3.1

Step 1.1 gives continuity and injectivity, while step 2.1 gives surjectivity.

step 1.1step 2.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03Open item page →

The principal inverse tangent $\arctan:\mathbb R\to(-\pi/2,\pi/2)$

Definition

By Tangent is a continuous strictly increasing bijection from $(-\pi/2,\pi/2)$ onto $\mathbb R$ , tangent restricts to a continuous strictly increasing bijection

$\tan:(-\pi/2,\pi/2)\longrightarrow\mathbb R.$

Its inverse is the principal inverse tangent

$\arctan:\mathbb R\longrightarrow(-\pi/2,\pi/2).$

Thus $\tan(\arctan y)=y$ for every real $y$ , while $\arctan(\tan x)=x$ precisely for $x$ in the displayed principal interval. The inverse is continuous and strictly increasing by Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f[I]$ , and the inverse $g : f[I] \to I$ is continuous and strictly monotone in the same sense as $f$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series

Statement

For every $x\in\mathbb R$ ,

$\frac{d}{dx}\arctan x=\frac1{1+x^2},\qquad \arctan x=\int_0^x\frac{dt}{1+t^2}.$

For $|x|<1$ ,

$\arctan x=\sum_{n=0}^{\infty}\frac{(-1)^n x^{2n+1}}{2n+1}.$

At the endpoint, the ordinarily convergent alternating series satisfies

$\frac\pi4=1-\frac13+\frac15-\frac17+\cdots.$

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Principal arctangent is the continuous increasing inverse of tangent on $(-\pi/2,\pi/2)$ (The principal inverse tangent $\arctan:\mathbb R\to(-\pi/2,\pi/2)$ ).

[L2]

The derivative of an inverse is the reciprocal of the original derivative when the latter is nonzero (Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f'(c) \ne 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)$ ).

[L3]

$(\tan u)'=\sec^2u=1+\tan^2u$ on the tangent domain, and $\tan0=0$ because $\sin0=0$ , $\cos0=1$ , and $\tan0=\sin0/\cos0$ (Tangent, cotangent, secant, and cosecant on their exact natural domains, The derivatives of sine and cosine are cosine and minus sine, Derivatives and fundamental periods of tangent, cotangent, secant, and cosecant, Pythagorean and parity identities for all six trigonometric functions on their natural domains).

[L4]

A continuous integrand has the integral-function derivative asserted by the first fundamental theorem. Oriented integrals reverse sign and are additive over arbitrary successive endpoints (A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The first fundamental theorem: if $f$ is integrable on $[a,b]$ and continuous at $c$ , then $F'(c) = f(c)$ ; in particular a continuous $f$ has $F$ as a primitive, The integral with oriented limits: $\int_a^a f := 0$ and $\int_b^a f := -\int_a^b f$ , For $a<c<b$ : $f$ is integrable on $[a,b]$ if and only if it is integrable on $[a,c]$ and on $[c,b]$ , and then $\int_a^b f = \int_a^c f + \int_c^b f$ ; with the oriented form for arbitrary $a,b,c$ ).

[L5]

For $|r|<1$ , $\sum_{n\ge0}r^n=1/(1-r)$ , and a real power series may be integrated termwise on compact subintervals of its convergence interval (For $|r| < 1$ , $\sum_{k \ge 0} r^k = 1/(1-r)$ , and for $|r| \ge 1$ the series diverges, Inside its radius a real power series may be integrated term by term on every closed subinterval).

[L6]

The alternating series $\sum_{n\ge0}(-1)^n/(2n+1)$ converges, and Abel's limit theorem identifies its sum with the radial limit of its power series (The alternating series test: if $(b_k)$ is nonincreasing with $b_k \to 0$ then $\sum_{k} (-1)^{k} b_k$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_n$ , Abel's limit theorem: if a real series converges to $s$ , then its power series tends to $s$ as $x\uparrow1$ ).

[L7]

The cofunction identities and the Pythagorean identity give $\tan(\pi/4)=1$ (Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions, Pythagorean and parity identities for all six trigonometric functions on their natural domains).

[L8]

Continuous functions are closed under the algebra used below; differentiable functions are continuous; and two continuous functions on an interval with the same derivative differ by a constant (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, A function differentiable at $c$ is continuous at $c$ , A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

Proof

technique · direct

1.1

For $y\in\mathbb R$ , put $u:=\arctan y$ . Then $\tan u=y$ and [L3] gives $(\tan)'(u)=1+y^2>0$ . Applying [L2] to the principal branch proves $(\arctan y)'=1/(1+y^2)$ .

L1L2L3

2.1

The function $t\mapsto1/(1+t^2)$ is continuous. By [L4], its oriented integral from $0$ to $x$ has derivative $1/(1+x^2)$ and value $0$ at $x=0$ . By [L3], $\tan0=0$ , so the inverse identity in [L1] gives $\arctan0=0$ ; step 1.1 gives its derivative and [L8] makes it continuous. Their difference is therefore continuous on $\mathbb R$ with zero derivative, so [L8] makes it zero.

step 1.1L1L3L4L8

3.1

If $|t|<1$ , [L5] with $r=-t^2$ gives $\frac1{1+t^2}=\sum_{n=0}^{\infty}(-1)^nt^{2n}.$ Termwise integration between $0$ and $x$ (reversing endpoints when $x<0$ ) and step 2.1 give the asserted arctangent series for $|x|<1$ .

step 2.1L5

4.1

Let $S:=\sum_{n\ge0}(-1)^n/(2n+1)$ , which exists by [L6]. Abel's theorem and step 3.1 yield $S=\lim_{x\uparrow1}\sum_{n\ge0}\frac{(-1)^nx^{2n+1}}{2n+1} =\lim_{x\uparrow1}\arctan x=\arctan1.$ By [L7] and the principal range, $\arctan1=\pi/4$ .

step 3.1L1L6L7

5.1

Steps 1.1–4.1 establish all four displayed claims.

step 1.1step 2.1step 3.1step 4.1∎

5 · Examples, counterexamples and false statements

None yet.

Sources

Standard references

Recommended treatments; not extraction sources.

Further Trigonometric Identities and Inverse Functions

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Principal inverse sine and inverse cosine

Definition

For −1<y<1-1<y<1−1<y<1, (arcsin⁡y)′=1/1−y2(\arcsin y)^{\prime}=1/\sqrt{1-y^2}(arcsiny)′=1/1−y2​ and (arccos⁡y)′=−1/1−y2(\arccos y)^{\prime}=-1/\sqrt{1-y^2}(arccosy)′=−1/1−y2​

Statement

Facts & Assumptions

Proof

Tangent is a continuous strictly increasing bijection from (−π/2,π/2)(-\pi/2,\pi/2)(−π/2,π/2) onto R\mathbb RR

Statement

Facts & Assumptions

Proof

The principal inverse tangent arctan⁡:R→(−π/2,π/2)\arctan:\mathbb R\to(-\pi/2,\pi/2)arctan:R→(−π/2,π/2)

Definition

Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources

Standard references

For $-1<y<1$ , $(\arcsin y)^{\prime}=1/\sqrt{1-y^2}$ and $(\arccos y)^{\prime}=-1/\sqrt{1-y^2}$

Tangent is a continuous strictly increasing bijection from $(-\pi/2,\pi/2)$ onto $\mathbb R$

The principal inverse tangent $\arctan:\mathbb R\to(-\pi/2,\pi/2)$