apply rem_sum_le_of_const (primeInterSieve x y z hz) 5 ?_
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∑ d ∈ (primeInterSieve x y z hz).prodPrimes.divisors,
      if ↑d ≤ z then 3 ^ ω d * |(primeInterSieve x y z hz).rem d| else 0) ≤
    5 * z * (1 + z.log) ^ 3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ d > 0, |(primeInterSieve x y z hz).rem d| ≤ 5