Compfiles/Imo2013P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2013, Problem 1

Prove that for any pair of positive integers k and n, there exist k positive integers m₁, m₂, ..., mₖ (not necessarily different) such that

1 + (2ᵏ - 1)/ n = (1 + 1/m₁) * (1 + 1/m₂) * ... * (1 + 1/mₖ).

Imports (4)
Imported by 1 file
  1. theorem Imo2013P1.prod_lemma line 40 source

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

    Statement uses: Nat, PNat, Eq, Rat, Finset.prod, Finset.range, HAdd.hAdd, OfNat.ofNat, HDiv.hDiv, ite, LT.lt

    Proof uses: Membership.mem, Finset, of_eq_true, Eq.trans, Inv.inv, True, congr, congrArg, ite_eq_left_of_eq_true, eq_true, Iff.mp, Finset.mem_range, one_div, eq_self, Finset.prod_congr, rfl

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. problem Imo2013P1.imo2013_p1 line 50 source

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

    Statement uses: PNat, Nat, Exists, Eq, Rat, HAdd.hAdd, OfNat.ofNat, HDiv.hDiv, HSub.hSub, HPow.hPow, Finset.prod, Finset.range

    Proof uses: Nat.recAux, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', pow_zero, sub_self, zero_div, add_zero, EmptyCollection.emptyCollection, Finset, Finset.card, funext, Nat.cast_one, div_self, Not, False and 140 more

    181 instances, coercions and auxiliary constants left out.

    Tactic trace: 50 steps

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