English
Let a, b, c, d, n ∈ ℕ and z ∈ ℝ. If z ≤ sqrtTwoAddSeries(a/b, n), b > 0, d > 0, and a^2 d ≤ (2d + c) b^2, then z ≤ sqrtTwoAddSeries(c/d, n+1).
Русский
Пусть a, b, c, d, n ∈ ℕ, z ∈ ℝ. Если z ≤ sqrtTwoAddSeries(a/b, n), b > 0, d > 0 и a^2 d ≤ (2d + c) b^2, то z ≤ sqrtTwoAddSeries(c/d, n+1).
LaTeX
$$$\\forall a,b,c,d,n\\in\\mathbb{N},\\; z\\in\\mathbb{R},\\; z \\le \\sqrtTwoAddSeries\\left(\\frac{a}{b}\\right) n \\land 0 < b \\land 0 < d \\land a^{2} d \\le (2d + c) b^{2} \\Rightarrow z \\le \\sqrtTwoAddSeries\\left(\\frac{c}{d}\\right) (n+1).$$$
Lean4
theorem pi_lt_d6 : π < 3.141593 := by
-- bound[3141593*^-6, Iters -> 11, Rounding -> .5, Precision -> 17]
pi_upper_bound [35839 / 25342, 49143 / 26596, 145729 / 74292, 294095 / 147759, 2 - 137 / 56868, 2 - 471 / 781921,
2 - 153 / 1015961, 2 - 157 / 4170049, 2 - 28 / 2974805, 2 - 9 / 3824747, 2 - 7 / 11899211]
