Mertens product upper bound (3.29), finite range $286 \le x < 700$

For every real number $x$ with $286 \le x < 700$,

where the product runs over the primes $p \le x$ and $\gamma$ denotes the Euler–Mascheroni constant.

This theorem is the finite-range leg of Rosser and Schoenfeld's proof of the Mertens product upper bound (3.29): in their proof of Theorem 8 (p. 70) the range $x \le 16{,}000$ is disposed of by direct tabulation, and the present statement covers the part $286 \le x < 700$ of that tabulation for which no analytic substitute is available. It is provable by a finite certified computation: the left-hand side is a finite product of exact rational values, while the right-hand side can be bounded below using rational approximations to $\log x$ and $e^{\gamma}$.

Formalization Note. The product is written as ∏ p ∈ Nat.primesLE ⌊x⌋₊, (p : ℝ) / ((p : ℝ) - 1), the finite set of primes at most the natural floor of $x$, and the right-hand side is Real.exp Real.eulerMascheroniConstant * Real.log x * (1 + 1 / (2 * (Real.log x) ^ 2)), matching the parent target's formulation.