theorem Erdos312.erdos_312 : (∃ (c : ℝ), 0 < c ∧ ∀ (K : ℝ), 1 < K → ∃ (N₀ : ℕ), ∀ (n : ℕ) (a : Fin n → ℕ), n ≥ N₀ ∧ ∑ i : Fin n, (↑(a i))⁻¹ > K → ∃ (S : Finset (Fin n)), 1 - Real.exp (-(c * K)) < ∑ i ∈ S, (↑(a i))⁻¹ ∧ ∑ i ∈ S, (↑(a i))⁻¹ ≤ 1) ↔ sorry

Does there exist a constant c > 0 such that, for any K > 1, whenever A is a sufficiently large finite multiset of integers with ∑ n ∈ A, 1/n > K there exists some S ⊆ A such that 1 - exp (-(c*K)) < ∑ n ∈ S, 1/n ≤ 1?