English
Let a, b, c, d, n be natural numbers and z a real number. 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), 0 < b, 0 < d и 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 sqrtTwoAddSeries_step_down (a b : ℕ) {c d n : ℕ} {z : ℝ} (hz : z ≤ sqrtTwoAddSeries (a / b) n) (hb : 0 < b)
(hd : 0 < d) (h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2) : z ≤ sqrtTwoAddSeries (c / d) (n + 1) :=
by
apply le_trans hz; rw [sqrtTwoAddSeries_succ]; apply sqrtTwoAddSeries_monotone_left
apply le_sqrt_of_sq_le
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
rw [div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hd'), div_le_div_iff₀ (pow_pos hb' _) hd']
exact mod_cast h
