no goals
x : ℝ
⊢ sqrtTwoAddSeries 0 0 < 2
norm_num
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < sqrt (2 ^ 2)
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < 2
refine' lt_of_lt_of_le _ (sqrt_sq zero_lt_two.le).le
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2

x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < sqrt (2 ^ 2)
rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']
x : ℝ
n : ℕ
⊢ 2 ≤ 2 ^ 2 - 2
x : ℝ
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2
refine' (sqrtTwoAddSeries_lt_two n).trans_le _
no goals
x : ℝ
n : ℕ
⊢ 2 ≤ 2 ^ 2 - 2
norm_num
no goals
x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
exact add_nonneg zero_le_two (sqrtTwoAddSeries_zero_nonneg n)