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) ≤ sqrtTwoAddSeries (↑c / ↑d) n
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
refine' le_trans _ hz
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 (sqrt (2 + ↑a / ↑b)) n ≤ sqrtTwoAddSeries (↑c / ↑d) n
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) ≤ sqrtTwoAddSeries (↑c / ↑d) n
rw [sqrtTwoAddSeries_succ]
case h
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
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
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 (sqrt (2 + ↑a / ↑b)) n ≤ sqrtTwoAddSeries (↑c / ↑d) n
apply sqrtTwoAddSeries_monotone_left
case h
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
hb' : 0 < ↑b
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
case h
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
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
case h
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
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
case h
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
hb' : 0 < ↑b
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
case h
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
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) * ↑d ^ 2 ≤ ↑c ^ 2 * ↑b
case h
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
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
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' _)]
no goals
case h
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
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) * ↑d ^ 2 ≤ ↑c ^ 2 * ↑b
exact_mod_cast h