Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1975P1

import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 1975, Problem 1
a) Prove that
$[5x]+[5y]\ge [3x+y]+[3y+x]$,

where $x,y\ge 0$ and $[u]$ denotes the greatest integer $\le u$ (e.g., $[\sqrt{2}]=1$).

(b) Using (a) or otherwise, prove that
$\frac{(5m)!(5n)!}{m!n!(3m+n)!(3n+m)!}$

is integral for all positive integral $m$ and $n$.
-/

namespace Usa1975P1

theorem usa1975_p1a (x y: ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : ⌊3*x + y⌋ + ⌊3*y + x⌋ ≤ ⌊5*x⌋ + ⌊5*y⌋ := sorry

open scoped Nat

theorem usa1975_p1b (m n : ℕ) : (m ! * n ! * (3*m+n) ! * (3*n+m) !) ∣ ((5*m)! * (5*n)!) := sorry

end Usa1975P1

File author(s): Pacmanboss256, hillosanation

This problem has a complete formalized solution.