simp only [div_eq_zero_iff, Nat.cast_eq_zero, Real.log_eq_zero, Nat.cast_eq_one, or_self_left,
  Finset.card_eq_zero, forall_eq_or_imp, Finset.range_zero, Finset.filter_empty, Finset.range_one,
  true_and]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (n : ℕ), ↑n / (↑n).log = 0 → ↑(Finset.filter IsPrimePow (Finset.range n)).card = 0
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ Finset.filter IsPrimePow {0} = ∅ ∧ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅