intro a ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (a : ℕ), ↑a = -1 → Finset.filter IsPrimePow (Finset.range a) = ∅
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a : ℕ
ha : ↑a = -1
⊢ Finset.filter IsPrimePow (Finset.range a) = ∅