Compfiles/Usa1975P1.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

9 declarations, 0 contain sorry, 0 declared as axioms

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$.

Imports (2)
Imported by 1 file
  1. lemma Nat.Prime.multiplicity_factorial Documented declaration: multiplicity_factorial line 34 source

    Source comment

    Solution adapted from Art of Problem Solving from https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Sylvester-Schur.3A.20.20p-adic.20valuation/near/525085669

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Nat.Prime, LT.lt, Nat.log, Eq, multiplicity, Nat.factorial, Finset.sum, Finset.Ico, OfNat.ofNat, HDiv.hDiv, HPow.hPow

    Proof uses: multiplicity_eq_of_emultiplicity_eq_some, Nat.Prime.emultiplicity_factorial

    22 instances, coercions and auxiliary constants left out.

    lemma Nat.Prime.multiplicity_factorial {p : ℕ} (hp : Prime p) {n b : ℕ} (h : log p n < b) :
  multiplicity p n.factorial = ∑ i ∈ Finset.Ico 1 b, n / p ^ i :=
…

    Mentions: h

  2. lemma Int.intCast_add_floor line 38 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Int, Eq, Int.floor, HAdd.hAdd

    Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, add_comm, Int.floor_add_intCast, eq_self

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  3. lemma Int.div_eq_floor line 41 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Eq, Int, HDiv.hDiv, Int.floor, Real

    Proof uses: Eq.mpr, id, congrArg, Int.floor_div_natCast, Int.floor_natCast, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  4. def trunCeil line 46 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Int

    Proof uses: HSub.hSub, Int.ceil, OfNat.ofNat

    6 instances, coercions and auxiliary constants left out.

  5. lemma floor_le_trunCeil line 49 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LT.lt, LE.le, Int, Int.floor, trunCeil

    Proof uses: Eq.mpr, Int.ceil, id, Eq, Int.floor_lt_ceil_of_lt

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  6. lemma cases line 52 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Int, HAdd.hAdd, trunCeil, HDiv.hDiv, Real, HMul.hMul

    Proof uses: List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.mpr, Int.ceil, id, Eq.trans, HSub.hSub and 79 more

    127 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  7. lemma h line 55 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, Int, HAdd.hAdd, Int.floor, HMul.hMul, OfNat.ofNat, Nat

    Proof uses: And, Eq, Not, Or, Classical.em, id, LT.lt, Eq.mp, congr, congrArg, Eq.trans, Membership.mem, Set, Set.Ico, True, congrFun', eq_true, true_and, Eq.mpr, And.left and 119 more

    175 instances, coercions and auxiliary constants left out.

    Tactic trace: 54 steps

    Open to load the checked before-and-after goal states.

  8. problem Usa1975P1.usa1975_p1a line 99 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, Int, HAdd.hAdd, Int.floor, HMul.hMul, Nat

    Proof uses: le_trans, Eq.mpr, id, Eq, Eq.trans, Function.swap, Int.add_nonneg, Iff.mpr, Int.floor_nonneg, h

    71 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  9. problem Usa1975P1.usa1975_p1b line 105 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Dvd.dvd, HMul.hMul, Nat.factorial, HAdd.hAdd, OfNat.ofNat

    Proof uses: Eq.mpr, Nat.Prime, HPow.hPow, id, Eq, congrArg, propext, Nat.dvd_iff_prime_pow_dvd_dvd, Ne, Nat.Prime.ne_one, Fact, Fact.mk, LE.le, padicValNat, Nat.pow_dvd_iff_le_padicValNat, of_eq_true, Not, Eq.trans, False, True and 79 more

    121 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

    Open to load the checked before-and-after goal states.