no goals
x : ℂ
hx : ↑abs x ≤ 1
⊢ ↑abs (exp x - 1 - x) = ↑abs (exp x - ∑ m in range 2, x ^ m / ↑(Nat.factorial m))
simp [sub_eq_add_neg, sum_range_succ_comm, add_assoc]
no goals
x : ℂ
hx : ↑abs x ≤ 1
⊢ 0 < 2
decide
case h
x : ℂ
hx : ↑abs x ≤ 1
⊢ ↑(Nat.succ 2) * (↑(Nat.factorial 2) * ↑2)⁻¹ ≤ 1
x : ℂ
hx : ↑abs x ≤ 1
⊢ ↑abs x ^ 2 * (↑(Nat.succ 2) * (↑(Nat.factorial 2) * ↑2)⁻¹) ≤ ↑abs x ^ 2 * 1
gcongr
no goals
case h
x : ℂ
hx : ↑abs x ≤ 1
⊢ ↑(Nat.succ 2) * (↑(Nat.factorial 2) * ↑2)⁻¹ ≤ 1
norm_num
no goals
x : ℂ
hx : ↑abs x ≤ 1
⊢ ↑abs x ^ 2 * 1 = ↑abs x ^ 2
rw [mul_one]