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