n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n)
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a < π
refine' lt_of_le_of_lt _ (pi_gt_sqrtTwoAddSeries n)
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ sqrt (2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n)
rw [mul_comm]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ (a / 2 ^ (n + 1)) ^ 2 ≤ 2 - sqrtTwoAddSeries 0 n
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ sqrt (2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)
refine' (div_le_iff (pow_pos (by norm_num) _ : (0 : ℝ) < _)).mp (le_sqrt_of_sq_le _)
no goals
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ (a / 2 ^ (n + 1)) ^ 2 ≤ 2 - sqrtTwoAddSeries 0 n
rwa [le_sub_comm, show (0 : ℝ) = (0 : ℕ) / (1 : ℕ) by rw [Nat.cast_zero, zero_div]]
no goals
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 < 2
norm_num
no goals
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 = ↑0 / ↑1
rw [Nat.cast_zero, zero_div]