English
Let p, q, r be positive integers. The inequality 1 < (1/p + 1/q + 1/r) holds if and only if the multiset {p, q, r} is admissible, i.e., it is one of {1, q, r}, {2, 2, r}, {2, 3, 3}, {2, 3, 4}, or {2, 3, 5}.
Русский
Пусть p, q, r — положительные целые числа. Неравенство 1 < (1/p + 1/q + 1/r) выполняется тогда и только тогда, когда мультимножество {p, q, r} допустимо, то есть равно одному из: {1, q, r}, {2, 2, r}, {2, 3, 3}, {2, 3, 4}, {2, 3, 5}.
LaTeX
$$$1 < \\sumInv\\{ p, q, r \\} \\quad\\Longleftrightarrow\\quad Admissible\\{ p, q, r \\}$$$
Lean4
/-- A multiset `{p,q,r}` of positive natural numbers
is a solution to `(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1` if and only if
it is `admissible` which means it is one of:
* `A' q r := {1,q,r}`
* `D' r := {2,2,r}`
* `E6 := {2,3,3}`, or `E7 := {2,3,4}`, or `E8 := {2,3,5}`
-/
theorem classification (p q r : ℕ+) : 1 < sumInv { p, q, r } ↔ Admissible { p, q, r } :=
⟨admissible_of_one_lt_sumInv, Admissible.one_lt_sumInv⟩
