no goals
ι : Type u_2
κ : Type ?u.55666
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : Summable f
⊢ (∑' (i : ι), f i) ≠ 0 ↔ ∃ x, f x ≠ 0
rw [Ne.def, tsum_eq_zero_iff hf, not_forall]