rwa [neg_ne_zero]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
⊢ -x ≠ 0
no goals