Compfiles/Imo1983P5.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1983, Problem 5

Is it possible to choose $1983$ distinct positive integers, all less than or equal to $10^5$, no three of which are consecutive terms of an arithmetic progression? Justify your answer.

Imports (3)
Imported by 1 file
  1. lemma Imo1983P5.Nat.ofDigits_eq line 31 source

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

    Statement uses: Nat, List, Eq, Nat.ofDigits, Finset.sum, Finset.range, List.length, HMul.hMul, List.getI, HPow.hPow

    Proof uses: List.rec, of_eq_true, OfNat.ofNat, List.nil, Eq.trans, True, congrArg, EmptyCollection.emptyCollection, Finset, funext, MulZeroClass.zero_mul, Finset.sum_const_zero, eq_self, Eq.mpr, List.cons, HAdd.hAdd, id, Finset.sum_range_succ', pow_zero, mul_one and 36 more

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  2. lemma Imo1983P5.Nat.getI_digits_lt line 42 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, List.getI, Nat.digits

    Proof uses: Eq.mpr, HMod.hMod, HDiv.hDiv, HPow.hPow, id, Eq, congrFun', congrArg, Nat.getD_digits, Nat.mod_lt

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. lemma Imo1983P5.Nat.getI_digits_add line 46 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, List.getI, Nat.digits, Eq

    Proof uses: Nat.strong_induction_on, dite, Or, of_eq_true, Eq.trans, True, forall_congr, congr, congrArg, congrFun', List.nil, List, Nat.digits_zero, zero_add, eq_self, implies_true, Eq.symm, add_zero, Not, Eq.mpr and 24 more

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  4. lemma Imo1983P5.Nat.eq_iff_getI_digits_eq line 76 source

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

    Statement uses: Nat, Iff, Eq, List.getI, Nat.digits

    Proof uses: Iff.intro, Eq.mpr, id, congrArg, Eq.refl, Nat.ofDigits, Eq.symm, Nat.ofDigits_digits, Finset.sum, Finset.range, List.length, HMul.hMul, HPow.hPow, Imo1983P5.Nat.ofDigits_eq, Union.union, Finset, SDiff.sdiff, Inter.inter, Finset.sdiff_union_inter, HAdd.hAdd and 22 more

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  5. def Imo1983P5.base_two_to_base_three line 111 source

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

    Statement uses: Nat

    Proof uses: Nat.ofDigits, OfNat.ofNat, Nat.digits

    2 instances, coercions and auxiliary constants left out.

  6. lemma Imo1983P5.digits_base_two_to_base_three line 113 source

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

    Statement uses: Nat, Eq, List, Nat.digits, OfNat.ofNat, Imo1983P5.base_two_to_base_three

    Proof uses: Eq.symm, Eq.mpr, Nat.ofDigits, id, congrArg, Imo1983P5.base_two_to_base_three.eq_1, Nat.digits_ofDigits, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Membership.mem, lt_trans, Nat.digits_lt_base, Ne, List.nil, Nat.getLast_digit_ne_zero, Iff.mp, Nat.digits_ne_nil_iff_ne_zero

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  7. lemma Imo1983P5.base_two_to_base_three_inj line 120 source

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

    Statement uses: Function.Injective, Nat, Imo1983P5.base_two_to_base_three

    Proof uses: Eq, Iff.mp, List, Nat.digits, OfNat.ofNat, Nat.digits_inj_iff, Eq.mpr, id, congrArg, Imo1983P5.digits_base_two_to_base_three, Eq.refl

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. lemma Imo1983P5.base_two_to_base_three_zero line 123 source

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

    Statement uses: Eq, Nat, Imo1983P5.base_two_to_base_three, OfNat.ofNat

    Proof uses: rfl

    2 instances, coercions and auxiliary constants left out.

  9. lemma Imo1983P5.base_two_to_base_three_pos line 125 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1983P5.base_two_to_base_three

    Proof uses: Nat.pos_of_ne_zero, Eq.rec, Eq, Ne, Function.Injective.ne, Imo1983P5.base_two_to_base_three_inj, LT.lt.ne', Imo1983P5.base_two_to_base_three_zero

    5 instances, coercions and auxiliary constants left out.

  10. def Imo1983P5.zero_or_one_in_base_three line 128 source

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

    Statement uses: Nat

    Proof uses: Or, Eq, List.getI, Nat.digits, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  11. lemma Imo1983P5.zero_or_one_in_base_three_of_eq_base_two_to_base_three line 131 source

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

    Statement uses: Nat, Eq, Imo1983P5.base_two_to_base_three, Imo1983P5.zero_or_one_in_base_three

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, Or, List.getI, Nat.digits, OfNat.ofNat, Imo1983P5.zero_or_one_in_base_three.eq_1, LE.le, propext, Nat.le_one_iff_eq_zero_or_eq_one, List, Imo1983P5.digits_base_two_to_base_three, LT.lt, Nat.succ, Nat.lt_succ_iff, Imo1983P5.Nat.getI_digits_lt, le_refl

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  12. lemma Imo1983P5.eq_iff_of_zero_or_one_in_base line 141 source

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

    Statement uses: Nat, Imo1983P5.zero_or_one_in_base_three, Iff, Or, Eq, List.getI, Nat.digits, OfNat.ofNat, HAdd.hAdd

    Proof uses: Eq.mpr, id, congrArg, propext, Imo1983P5.Nat.eq_iff_getI_digits_eq, LT.lt, Eq.mp, Imo1983P5.zero_or_one_in_base_three.eq_1, Iff.intro, Imo1983P5.Nat.getI_digits_add, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  13. theorem Imo1983P5.generalized line 153 source

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

    Statement uses: PNat, Exists, Finset, And, Eq, Nat, Finset.card, HSub.hSub, HPow.hPow, OfNat.ofNat, Membership.mem, LE.le, HDiv.hDiv, LT.lt, Ne, HAdd.hAdd, HMul.hMul

    Proof uses: Exists.intro, Finset.map, Subtype, SDiff.sdiff, Finset.range, Function.Embedding.mk, Subtype.mk, Imo1983P5.base_two_to_base_three, Imo1983P5.base_two_to_base_three_pos, Subtype.ext, Imo1983P5.base_two_to_base_three_inj, congrArg, Finset.attach, And.intro, Eq.mpr, id, Finset.card_map, Finset.card_attach, Inter.inter, Finset.card_sdiff and 72 more

    136 instances, coercions and auxiliary constants left out.

    Tactic trace: 55 steps

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

  14. problem Imo1983P5.imo1983_p5 line 202 source

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

    Statement uses: Exists, Finset, PNat, And, Eq, Nat, Finset.card, OfNat.ofNat, Membership.mem, LE.le, HPow.hPow, LT.lt, Ne, HAdd.hAdd, HMul.hMul

    Proof uses: HSub.hSub, HDiv.hDiv, Imo1983P5.generalized, Eq.mpr, id, congrArg, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true, Finset.exists_subset_card_eq, Exists.intro, And.intro, Eq.symm, propext, PNat.coe_le_coe, le_trans

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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