English
Let n be a natural number and S the sum of its proper divisors. If S divides n, then S equals 1 or S equals n.
Русский
Пусть n — натуральное число, S — сумма его правильных делителей. Если S делит n, то S равно 1 или S равно n.
LaTeX
$$$\displaystyle S = \sum_{x \in n.properDivisors} x \quad\text{and}\quad S \mid n \quad\Rightarrow\quad S = 1 \ \/\= S = n.$$$
Lean4
theorem sum_properDivisors_dvd (h : (∑ x ∈ n.properDivisors, x) ∣ n) :
∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n :=
by
rcases n with - | n
· simp
· rcases n with - | n
· simp at h
· rw [or_iff_not_imp_right]
intro ne_n
have hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ :=
lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n
symm
rw [← mem_singleton,
eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2 (mem_properDivisors.2 ⟨h, hlt⟩))
(sum_singleton _ _),
mem_properDivisors]
exact ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩
