English
For n in N, IsPrimePow(n) iff there exist p and k with p ≤ n, k ≤ n, p prime, k > 0, and p^k = n.
Русский
Для n ∈ ℕ: IsPrimePow(n) эквивалентно существованию p, k такие, что p ≤ n, k ≤ n, p простое, k > 0 и p^k = n.
LaTeX
$$$IsPrimePow(n) \iff \exists p \le n, \exists k \le n, (p \text{ Prime}) \land 0 < k \land p^k = n$$$
Lean4
theorem isPrimePow_nat_iff_bounded (n : ℕ) :
IsPrimePow n ↔ ∃ p : ℕ, p ≤ n ∧ ∃ k : ℕ, k ≤ n ∧ p.Prime ∧ 0 < k ∧ p ^ k = n :=
by
rw [isPrimePow_nat_iff]
refine Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, ?_⟩
rintro ⟨p, k, hp, hk, rfl⟩
refine ⟨p, ?_, k, (Nat.lt_pow_self hp.one_lt).le, hp, hk, rfl⟩
conv => {lhs; rw [← (pow_one p)]}
exact Nat.pow_le_pow_right hp.one_lt.le hk
