Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1982P2

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Polynomial.Roots
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Analysis.Normed.Field.Basic
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Order.Interval.Set.Infinite
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Positivity.Core
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1982, Problem 2

Show that if m, n are positive integers such that
(x^(m+n) + y^(m+n) + z^(m+n))/(m+n) =
((x^m + y^m + z^m)/m) ((x^n + y^n + z^n)/n)
for all real x, y, z with sum 0, then {m, n} = {2, 3} or {2, 5}.
-/

namespace Usa1982P2

open Polynomial

theorem usa1982_p2 (m n : ℕ) (hm : 0 < m) (hn : 0 < n)
    (h : ∀ x y z : ℝ, x + y + z = 0 →
      (x ^ (m + n) + y ^ (m + n) + z ^ (m + n)) / (m + n) =
        (x ^ m + y ^ m + z ^ m) / m * ((x ^ n + y ^ n + z ^ n) / n)) :
    (m = 2 ∧ n = 3) ∨ (m = 3 ∧ n = 2) ∨ (m = 2 ∧ n = 5) ∨ (m = 5 ∧ n = 2) := sorry

end Usa1982P2

File author(s): Kimi K3

This problem has a complete formalized solution.