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.

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

Statement

For every x∈R,

ddxarctan⁡x=11+x2,arctan⁡x=∫0xdt1+t2.

For ∣x∣<1,

arctan⁡x=∑n=0∞(−1)nx2n+12n+1.

At the endpoint, the ordinarily convergent alternating series satisfies

π4=1−13+15−17+⋯ .

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Principal arctangent is the continuous increasing inverse of tangent on (−π/2,π/2) (The principal inverse tangent arctan⁡:R→(−π/2,π/2)).

[L5]

For ∣r∣<1, ∑n≥0rn=1/(1−r), and a real power series may be integrated termwise on compact subintervals of its convergence interval (For ∣r∣<1, ∑k≥0rk=1/(1−r), and for ∣r∣≥1 the series diverges, Inside its radius a real power series may be integrated term by term on every closed subinterval).

Proof

technique · direct
1.1

For y∈R, put u:=arctan⁡y. Then tan⁡u=y and [L3] gives (tan⁡)′(u)=1+y2>0. Applying [L2] to the principal branch proves (arctan⁡y)′=1/(1+y2).

L1L2L3
2.1

The function t↦1/(1+t2) is continuous. By [L4], its oriented integral from 0 to x has derivative 1/(1+x2) and value 0 at x=0. By [L3], tan⁡0=0, so the inverse identity in [L1] gives arctan⁡0=0; step 1.1 gives its derivative and [L8] makes it continuous. Their difference is therefore continuous on R with zero derivative, so [L8] makes it zero.

step 1.1L1L3L4L8
3.1

If ∣t∣<1, [L5] with r=−t2 gives 11+t2=∑n=0∞(−1)nt2n. 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:=∑n≥0(−1)n/(2n+1), which exists by [L6]. Abel's theorem and step 3.1 yield S=lim⁡x↑1∑n≥0(−1)nx2n+12n+1=lim⁡x↑1arctan⁡x=arctan⁡1. By [L7] and the principal range, arctan⁡1=π/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∎

Depends on

Used by

Dependency tree · two levels

97 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