English
Let n be a natural number and s a finite subset of ℕ with s ⊆ the proper divisors of n. If the sum of the elements of s equals the sum of all proper divisors of n, then s is exactly the set of all proper divisors of n.
Русский
Пусть n — целое неотрицательное число и s — конечное подмножество ℕ такое, что s ⊆ правильных делителей n. Если сумма элементов s равна сумме всех правильных делителей n, то s совпадает с полным множеством правильных делителей n.
LaTeX
$$$\displaystyle \text{If } s \subseteq D(n) \ \land\ \sum_{x\in s} x = \sum_{x\in D(n)} x \text{ then } s = D(n).$$$
Lean4
theorem eq_properDivisors_of_subset_of_sum_eq_sum {s : Finset ℕ} (hsub : s ⊆ n.properDivisors) :
((∑ x ∈ s, x) = ∑ x ∈ n.properDivisors, x) → s = n.properDivisors :=
by
cases n
· rw [properDivisors_zero, subset_empty] at hsub
simp [hsub]
classical
rw [← sum_sdiff hsub]
intro h
apply Subset.antisymm hsub
rw [← sdiff_eq_empty_iff_subset]
contrapose h
rw [← Ne, ← nonempty_iff_ne_empty] at h
apply ne_of_lt
rw [← zero_add (∑ x ∈ s, x), ← add_assoc, add_zero]
apply add_lt_add_right
have hlt := sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset hx)
simp only [sum_const_zero] at hlt
apply hlt
