rw [abs_of_nonneg]
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
C : ℝ
N : ℕ
hN : ¬N = 0
⊢ 0 ≤ (↑N).log