x : ℝ
hx : abs' x ≤ 1
⊢ abs' (exp x - 1 - x) ≤ abs' x ^ 2
x : ℝ
hx : abs' x ≤ 1
⊢ abs' (exp x - 1 - x) ≤ x ^ 2
rw [← _root_.sq_abs]
x : ℝ
hx : abs' x ≤ 1
this : ↑Complex.abs ↑x ≤ 1
⊢ abs' (exp x - 1 - x) ≤ abs' x ^ 2
x : ℝ
hx : abs' x ≤ 1
⊢ abs' (exp x - 1 - x) ≤ abs' x ^ 2
have : Complex.abs x ≤ 1 := by exact_mod_cast hx
x : ℝ
hx : abs' x ≤ 1
this✝ : ↑Complex.abs ↑x ≤ 1
this : ↑Complex.abs (Complex.exp ↑x - 1 - ↑x) ≤ ↑Complex.abs ↑x ^ 2
⊢ abs' (exp x - 1 - x) ≤ abs' x ^ 2
x : ℝ
hx : abs' x ≤ 1
this : ↑Complex.abs ↑x ≤ 1
⊢ abs' (exp x - 1 - x) ≤ abs' x ^ 2
have := Complex.abs_exp_sub_one_sub_id_le this
x : ℝ
hx : abs' x ≤ 1
this✝ : ↑Complex.abs ↑x ≤ 1
this : abs' (exp x - 1 - x) ≤ abs' x ^ 2
⊢ abs' (exp x - 1 - x) ≤ abs' x ^ 2
x : ℝ
hx : abs' x ≤ 1
this✝ : ↑Complex.abs ↑x ≤ 1
this : ↑Complex.abs (Complex.exp ↑x - 1 - ↑x) ≤ ↑Complex.abs ↑x ^ 2
⊢ abs' (exp x - 1 - x) ≤ abs' x ^ 2
rw [← ofReal_one, ← ofReal_exp, ← ofReal_sub, ← ofReal_sub, abs_ofReal, abs_ofReal] at this
no goals
x : ℝ
hx : abs' x ≤ 1
this✝ : ↑Complex.abs ↑x ≤ 1
this : abs' (exp x - 1 - x) ≤ abs' x ^ 2
⊢ abs' (exp x - 1 - x) ≤ abs' x ^ 2
exact this
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs ↑x ≤ 1
exact_mod_cast hx