English
Let p be prime and k a natural number. Then x belongs to the proper divisors of p^k if and only if there exists a natural j with j < k and x = p^j.
Русский
Пусть p — простое число и k натуральное. Тогда x ∈ properDivisors(p^k) тогда и только тогда, когда существует j < k такое, что x = p^j.
LaTeX
$$$x \in \operatorname{properDivisors}(p^k) \iff \exists j (j < k) \land x = p^j.$$$
Lean4
theorem mem_properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} :
x ∈ properDivisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j :=
by
rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]
simp only [exists_prop, and_assoc]
apply exists_congr
intro a
constructor <;> intro h
· rcases h with ⟨_h_left, rfl, h_right⟩
rw [Nat.pow_lt_pow_iff_right pp.one_lt] at h_right
exact ⟨h_right, rfl⟩
· rcases h with ⟨h_left, rfl⟩
rw [Nat.pow_lt_pow_iff_right pp.one_lt]
simp [h_left, le_of_lt]
