rw [isPrimePow_nat_iff_bounded n] at hnprime
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : ∃ p ≤ n, ∃ k ≤ n, p.Prime ∧ 0 < k ∧ p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k