no goals
x : ℂ
hx : ↑abs x ≤ 1
⊢ ↑abs (exp x - 1) = ↑abs (exp x - ∑ m in range 1, x ^ m / ↑(Nat.factorial m))
simp [sum_range_succ]
no goals
x : ℂ
hx : ↑abs x ≤ 1
⊢ 0 < 1
decide
no goals
x : ℂ
hx : ↑abs x ≤ 1
⊢ ↑abs x ^ 1 * (↑(Nat.succ 1) * (↑(Nat.factorial 1) * ↑1)⁻¹) = 2 * ↑abs x
simp [two_mul, mul_two, mul_add, mul_comm, add_mul]