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

Given: No hypotheses beyond those quantified in the statement.

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)$).

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)$).

$(\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).

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$).

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).

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$).

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).

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).