English
Let c, d, a, b, n be natural numbers and z a real number. If sqrtTwoAddSeries(c/d, n) ≤ z, b > 0, d > 0, and (2b + a) d^2 ≤ c^2 b, then sqrtTwoAddSeries(a/b, n+1) ≤ z.
Русский
Пусть c, d, a, b, n ∈ нат. чисел, z ∈ ℝ. Если sqrtTwoAddSeries(c/d, n) ≤ z, 0 < b, 0 < d и (2b + a) d^2 ≤ c^2 b, тогда sqrtTwoAddSeries(a/b, n+1) ≤ z.
LaTeX
$$$\\forall c,d,a,b,n\\in\\mathbb{N}, z\\in\\mathbb{R},\\;\\sqrtTwoAddSeries\\left(\\frac{c}{d}\\right) n \\le z \\;\\land\\; 0 < b \\;\\land\\; 0 < d \\;\\land\\; (2b + a) d^2 \\le c^2 b \\Rightarrow \\; \\sqrtTwoAddSeries\\left(\\frac{a}{b}\\right) (n+1) \\le z.$$$
Lean4
theorem sqrtTwoAddSeries_step_up (c d : ℕ) {a b n : ℕ} {z : ℝ} (hz : sqrtTwoAddSeries (c / d) n ≤ z) (hb : 0 < b)
(hd : 0 < d) (h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b) : sqrtTwoAddSeries (a / b) (n + 1) ≤ z :=
by
refine le_trans ?_ hz; rw [sqrtTwoAddSeries_succ]; apply sqrtTwoAddSeries_monotone_left
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
rw [sqrt_le_left (div_nonneg c.cast_nonneg d.cast_nonneg), div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hb'),
div_le_div_iff₀ hb' (pow_pos hd' _)]
exact mod_cast h
