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: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Machin's formula $π / 4 = 4 \arctan (1 / 5) - \arctan (1 / 239)$

Example

Machin's formula is

$\frac{π}{4} = 4 \arctan \frac{1}{5} - \arctan \frac{1}{239} .$

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Principal arctangent takes values in $(- π / 2, π / 2)$ , is the inverse of tangent there, and is strictly increasing (The principal inverse tangent $\arctan : R \to (- π / 2, π / 2)$ , Tangent is a continuous strictly increasing bijection from $(- π / 2, π / 2)$ onto $R$ ).

[L2]

The tangent addition and subtraction formulas hold when their displayed denominators and domains are nonzero (Addition and subtraction formulas for tangent, cotangent, secant, and cosecant on their exact domains).

[L3]

Tangent is the quotient of sine by cosine; $\sin 0 = 0$ and $\cos 0 = 1$ ; and the cofunction and Pythagorean identities give $\tan (π / 4) = 1$ (Tangent, cotangent, secant, and cosecant on their exact natural domains, The derivatives of sine and cosine are cosine and minus sine, 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).

Proof

technique · direct

1.1

Put $a : = \arctan (1 / 5)$ and $b : = \arctan (1 / 239)$ . Then $\tan a = 1 / 5$ and $\tan b = 1 / 239$ . Comparing with $\tan 0 = 0$ and [L3] on the principal branch gives $0 < a, b < π / 4$ .

L1L3

2.1

Since $0 < a < π / 4$ , we have $0 < 2 a < π / 2$ , so the tangent addition formula applies. It gives $\tan (2 a) = \frac{5}{12} < 1 = \tan (π / 4) .$ Strict increase of tangent on the principal branch now gives $2 a < π / 4$ , hence $0 < 4 a < π / 2$ .

step 1.1L1L2L3algebra

3.1

The addition formula, now applied to $2 a + 2 a$ , gives $\tan (4 a) = \frac{120}{119} > 1.$ All displayed denominators are positive.

step 2.1L2algebra

4.1

A final use of [L2] gives $\tan (4 a - b) = \frac{120 / 119 - 1 / 239}{1 + (120 / 119) (1 / 239)} = 1.$ The denominator is positive.

step 1.1step 3.1L2algebra

4.2

By step 2.1, $4 a$ lies in the principal tangent interval. Since $\tan (4 a) > 1 = \tan (π / 4)$ , strict increase gives $4 a > π / 4 > b$ . Thus $0 < 4 a - b < 4 a < π / 2$ . Consequently $4 a - b$ and $π / 4$ lie in the same injective branch of tangent.

step 1.1step 2.1step 3.1L1L3

5.1

Steps 4.1 and 4.2 imply $4 a - b = π / 4$ , which is the claimed formula.

step 4.1step 4.2∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

$\arcsin (\sin x)$ is not the identity outside the principal interval

Example

The identity $\arcsin (\sin x) = x$ is not valid for every $x \in R$ . For example,

$\arcsin (\sin (3 π / 4)) = π / 4 \neq 3 π / 4.$

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Principal arcsine is the inverse of sine with values restricted to $[- π / 2, π / 2]$ (Principal inverse sine and inverse cosine).

[L2]

The supplementary identity is $\sin (π - x) = \sin x$ (Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions).

Proof

technique · direct

1.1

By [L2], $\sin (3 π / 4) = \sin (π / 4)$ . Since $π / 4$ lies in the principal range of arcsine, [L1] gives $\arcsin (\sin (3 π / 4)) = π / 4$ .

L1L2algebra

2.1

Since $π / 4 \neq 3 π / 4$ , step 1.1 is the claimed counterexample.

step 1.1algebra∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Principal arcsine has no finite derivative at $- 1$ or $1$

Example

The principal arcsine $\arcsin : [- 1, 1] \to [- π / 2, π / 2]$ has no finite derivative at either endpoint $1$ or $- 1$ (with the library's relative, one-sided endpoint convention).

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

On $[- 1, 1]$ , $\sin (\arcsin y) = y$ , and $\arcsin (1) = π / 2$ , $\arcsin (- 1) = - π / 2$ (Principal inverse sine and inverse cosine).

[L2]

The chain rule applies to derivatives relative to their domains (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[L3]

$(\sin x)^{'} = \cos x$ , while $\cos (π / 2) = \cos (- π / 2) = 0$ (The derivatives of sine and cosine are cosine and minus sine, Quarter-turn values and shifts by pi/2 and pi, Pythagorean and parity identities for all six trigonometric functions on their natural domains).

Proof

technique · contradiction

1.1

Suppose $\arcsin$ had a finite derivative at $1$ . Differentiate the identity $\sin (\arcsin y) = y$ at $1$ relative to $[- 1, 1]$ . The derivative of the right side is $1$ , whereas [L2] and [L3] make the derivative of the left side $\cos (π / 2) (\arcsin)^{'} (1) = 0$ , a contradiction.

assume-contraL1L2L3

1.2

The identical argument at $- 1$ gives $1 = \cos (- π / 2) (\arcsin)^{'} (- 1) = 0$ .

assume-contraL1L2L3

2.1

Therefore neither finite endpoint derivative exists.

step 1.1step 1.2discharge-contradiction∎

Further Trigonometric Identities and Inverse Functions: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Machin's formula π/4=4arctan⁡(1/5)−arctan⁡(1/239)π/4=4arctan(1/5)−arctan(1/239)

Example

Facts & Assumptions

Proof

arcsin⁡(sin⁡x)arcsin(sinx) is not the identity outside the principal interval

Example

Facts & Assumptions

Proof

Principal arcsine has no finite derivative at −1−1 or 11

Example

Facts & Assumptions

Proof

Sources

Machin's formula $π / 4 = 4 \arctan (1 / 5) - \arctan (1 / 239)$

$\arcsin (\sin x)$ is not the identity outside the principal interval

Principal arcsine has no finite derivative at $- 1$ or $1$