English
If n is prime, then n^m is deficient for all natural m.
Русский
Если n простое, то n^m дефицитно для всех натуральных m.
LaTeX
$$$\operatorname{Prime}(n) \Rightarrow \operatorname{Deficient}(n^{m})$$$
Lean4
/-- Any natural number power of a prime is deficient -/
theorem deficient_pow (h : Prime n) : Deficient (n ^ m) :=
by
rcases Nat.eq_zero_or_pos m with (rfl | _)
· simpa using deficient_one
· have h1 : (n ^ m).properDivisors = image (n ^ ·) (range m) :=
by
apply subset_antisymm <;> intro a
· simp only [mem_properDivisors, mem_image, mem_range, dvd_prime_pow h]
rintro ⟨⟨t, ht, rfl⟩, ha'⟩
exact ⟨t, lt_of_le_of_ne ht (fun ht' ↦ lt_irrefl _ (ht' ▸ ha')), rfl⟩
· simp only [mem_image, mem_range, mem_properDivisors, forall_exists_index, and_imp]
intro x hx hy
constructor
· rw [← hy, dvd_prime_pow h]
exact ⟨x, Nat.le_of_succ_le hx, rfl⟩
· rw [← hy]
exact (Nat.pow_lt_pow_iff_right (Prime.two_le h)).mpr hx
have h2 : ∑ i ∈ image (fun x => n ^ x) (range m), i = ∑ i ∈ range m, n ^ i :=
by
rw [Finset.sum_image]
rintro x _ y _
apply pow_injective_of_not_isUnit h.not_isUnit <| Prime.ne_zero h
rw [Deficient, h1, h2]
calc
∑ i ∈ range m, n ^ i = (n ^ m - 1) / (n - 1) := (Nat.geomSum_eq (Prime.two_le h) _)
_ ≤ (n ^ m - 1) := (Nat.div_le_self (n ^ m - 1) (n - 1))
_ < n ^ m := sub_lt (pow_pos (Prime.pos h) m) (Nat.one_pos)
