The Exercise

The exercise is an estimate from analysis about the primes $p = 2, 3, 5, 7, 11, \dots$ and the series of their inverse squares, $\frac14 + \frac19 + \frac1{25} + \frac1{49} + \cdots$ . It asks for an explicit upper bound on this series, and for two facts about the integral of $1/y^2$ beyond $y = 2$ : its value over the whole half line, and a lower bound on it over each interval of unit length.

The Claim

Theorem 1. For every real number $x \ge 2$ , $\int_x^{x+1} \frac{dy}{y^2} \;\ge\; \frac{2}{3x^2} .$ (1)^✦ The integral over the half line $y > 2$ is $\int_2^\infty \frac{dy}{y^2} = \frac12 ,$ (2)^✦ and the sum over all primes $p$ satisfies $\sum_{p\ \mathrm{prime}} \frac{1}{p^2} \;\le\; \frac34 .$ (3)^✦

What Is Checked

The claim is stated over the real numbers and the set of all primes, with no hypothesis beyond $x \ge 2$ in (1).

About them the library proves two facts of calculus, (1) and (2), and one about the primes, (3).