RS_prime.mertens_first_theorem'

@[blueprint  "rs-420"]theorem mertens_first_theorem' :    ∃ C, ∀ x ≥ 2, |∑ p ∈ filter Prime (Iic ⌊x⌋₊), Real.log p / p - Real.log x| ≤ C := by  obtain ⟨C, hC⟩ := pnt  refine ⟨|mertensConstant| + C / Real.log 2 ^ 2 +    ∫ y in Set.Ioi 2, |(θ y - y) / (y ^ 2)|, fun x hx => ?_⟩  calc  _ ≤ |mertensConstant + (θ x - x) / x - ∫ y in Set.Ioi x, (θ y - y) / (y ^ 2)| := by    rw [eq_420 hx]; ring_nf; rfl  _ ≤ |mertensConstant| + |(θ x - x) / x| + ∫ y in Set.Ioi x, |(θ y - y) / (y ^ 2)| := by    grw [sub_eq_add_neg, abs_add_le, abs_add_le, abs_neg, abs_integral_le_integral_abs]  _ ≤ _ := by    gcongr    · grw [abs_div, hC.2 x hx, abs_of_nonneg (by grind), div_right_comm,        mul_div_cancel_right₀ _ (by grind)]      ring_nf      gcongr      · exact hC.1      · exact inv_nonneg.2 (log_nonneg (by grind))    · filter_upwards with a      apply abs_nonneg    · simpa using integrableOn_deriv_inv.1.abs