English
An element a is a prime power iff aleph0 ≤ a or a is a prime power of a natural.
Русский
Элемент a является степенью простого числа тогда и только тогда, когда aleph0 ≤ a или a = p^k для натурального p.
LaTeX
$$IsPrimePow(a) ↔ (aleph0 ≤ a) ∨ ∃ n ∈ ℕ, a = n ∧ IsPrimePow(n)$$
Lean4
theorem isPrimePow_iff {a : Cardinal} : IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n : ℕ, a = n ∧ IsPrimePow n :=
by
by_cases h : ℵ₀ ≤ a
· simp [h, (prime_of_aleph0_le h).isPrimePow]
simp only [h, false_or, isPrimePow_nat_iff]
lift a to ℕ using not_le.mp h
rw [isPrimePow_def]
refine ⟨?_, fun ⟨n, han, p, k, hp, hk, h⟩ => ⟨p, k, nat_is_prime_iff.2 hp, hk, by rw [han]; exact mod_cast h⟩⟩
rintro ⟨p, k, hp, hk, hpk⟩
have key : p ^ (1 : Cardinal) ≤ ↑a := by rw [← hpk]; apply power_le_power_left hp.ne_zero; exact mod_cast hk
rw [power_one] at key
lift p to ℕ using key.trans_lt (nat_lt_aleph0 a)
exact ⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, mod_cast hpk⟩
