Erdos392.prod_one_sub_one_div_prime_tendsto_zero

lemma prod_one_sub_one_div_prime_tendsto_zero :    Filter.Tendsto      (fun n ↦ ∏ p ∈ filter Prime (range n), (1 - 1 / (p : ℝ)))      .atTop (nhds 0) := by  have h_exp_neg_sum : Filter.Tendsto      (fun n : ℕ ↦ Real.exp        (-∑ p ∈ filter Prime (range n), (1 / p : ℝ)))      .atTop (nhds 0) := by    have h_not_summable : ¬Summable (fun p : ℕ ↦ if p.Prime then (1 / p : ℝ) else 0) := by      have h_primes : ¬Summable (fun p : Nat.Primes ↦ (1 / p : ℝ)) := by        convert Primes.not_summable_one_div      contrapose! h_primes      convert! h_primes.comp_injective (fun a b h ↦ Subtype.ext h) using 1      ext ⟨p, hp⟩      simp [hp]    have h_diverge : Filter.Tendsto        (fun n : ℕ ↦ ∑ p ∈ range n, if p.Prime then (1 / p : ℝ) else 0) .atTop .atTop :=      (not_summable_iff_tendsto_nat_atTop_of_nonneg (fun _ ↦ by positivity)).mp h_not_summable    simpa [sum_filter] using h_diverge  refine squeeze_zero (fun n ↦ prod_nonneg fun _ hx ↦    sub_nonneg.mpr <| div_le_self zero_le_one <| mod_cast (mem_filter.mp hx).2.pos) ?_ h_exp_neg_sum  intro n  rw [exp_neg, exp_sum, ← prod_inv_distrib]  refine prod_le_prod (fun _ hx ↦ sub_nonneg.mpr <| div_le_self zero_le_one <|    mod_cast (mem_filter.mp hx).2.pos) fun _ _ ↦ ?_  rw [← Real.exp_neg]  exact (Real.add_one_le_exp _).trans' (by norm_num)