simp only [Finset.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_union, Finset.mem_image,
  Finset.mem_product, Prod.exists, and_imp]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (Finset.range N) →
    n ∈
      Finset.filter Nat.Prime (Finset.range N) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → IsPrimePow n → n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n