Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1973P5

module

public import Mathlib.Analysis.SpecialFunctions.Pow.Real
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Positivity.Basic
public import Mathlib.Tactic.Positivity.Core
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1973, Problem 5

Show that the cube roots of three distinct primes cannot be terms in an
arithmetic progression (whether consecutive or not).
-/

namespace Usa1973P5

-- If `∛p, ∛q, ∛r` are terms of an arithmetic progression with common
-- difference `d`, at integer positions differing by `m` and `n` from the
-- position of `∛p`, then `∛q = ∛p + m d` and `∛r = ∛p + n d` as below, so it
-- suffices to show that this is impossible for distinct primes `p, q, r`.
theorem usa1973_p5 (p q r : ℕ) (hp : p.Prime) (hq : q.Prime) (hr : r.Prime)
    (hpq : p ≠ q) (hqr : q ≠ r) (hpr : p ≠ r) :
    ¬∃ (m n : ℤ) (d : ℝ),
      (q : ℝ) ^ ((1 : ℝ) / 3) = (p : ℝ) ^ ((1 : ℝ) / 3) + (m : ℝ) * d ∧
      (r : ℝ) ^ ((1 : ℝ) / 3) = (p : ℝ) ^ ((1 : ℝ) / 3) + (n : ℝ) * d := sorry

end Usa1973P5

File author(s): Kimi K3

This problem has a complete formalized solution.