Compfiles/Imo1971P3.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1971, Problem 3

Prove that we can find an infinite set of positive integers of the form 2^n - 3 (where n is a positive integer) every pair of which are relatively prime.

Imports (2)
Imported by 1 file
  1. def Imo1971P3.pairwise_coprime_f line 33 source

    standard axioms: propext what this means

    Statement uses: Set, Nat

    Proof uses: Set.Pairwise, Nat.Coprime, HSub.hSub, HPow.hPow, OfNat.ofNat

    7 instances, coercions and auxiliary constants left out.

  2. def Imo1971P3.a line 36 source

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

    Statement uses: Nat

    2 instances, coercions and auxiliary constants left out.

  3. theorem Imo1971P3.a_ge_and_A_odd line 41 source

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

    Statement uses: Nat, And, LE.le, OfNat.ofNat, Imo1971P3.a, Odd, HSub.hSub, HPow.hPow

    Proof uses: Imo1971P3.a.induct_unfolding, And.intro, le_refl, Iff.mpr, Eq, HMod.hMod, Nat.odd_iff, rfl, HMul.hMul, Finset.prod, Nat.primeFactors, LT.lt, Eq.mpr, HAdd.hAdd, id, congrArg, propext, Nat.lt_iff_add_one_le, Finset.one_le_prod, Membership.mem and 91 more

    150 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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

  4. theorem Imo1971P3.A_ge' line 71 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, HPow.hPow, Imo1971P3.a

    Proof uses: Iff.mp, Nat.clog, Nat.clog_le_iff_le_pow, one_lt_two, Eq.mpr, id, Eq, congrArg, Eq.refl, And.left, Odd, HSub.hSub, Imo1971P3.a_ge_and_A_odd

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  5. theorem Imo1971P3.a_strictMono line 77 source

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

    Statement uses: StrictMono, Nat, Imo1971P3.a

    Proof uses: strictMono_nat_of_lt_succ, And, LE.le, OfNat.ofNat, Odd, HSub.hSub, HPow.hPow, Imo1971P3.a_ge_and_A_odd, Eq.mpr, LT.lt, HAdd.hAdd, Imo1971P3.a.match_1, Unit, HMul.hMul, Finset.prod, Nat.primeFactors, id, Eq, congrArg, Imo1971P3.a.eq_def and 26 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  6. theorem Imo1971P3.a_prime_lemma line 99 source

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

    Statement uses: Nat, LT.lt, Dvd.dvd, HSub.hSub, HPow.hPow, OfNat.ofNat, Imo1971P3.a, Nat.Prime

    Proof uses: Imo1971P3.a.induct_unfolding, False.elim, Eq.mp, False, Nat.succ, dite, HMul.hMul, Finset.prod, Nat.primeFactors, Eq, Nat.dvd_mul_left_of_dvd, Finset.dvd_prod_of_mem, Eq.mpr, Membership.mem, Finset, Not, id, Eq.trans, And, Ne and 7 more

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  7. theorem Imo1971P3.a_pairwise_coprime line 113 source

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

    Statement uses: Imo1971P3.pairwise_coprime_f, Set.range, Nat, Imo1971P3.a

    Proof uses: Membership.mem, Set, Ne, Nat.Coprime, HSub.hSub, HPow.hPow, OfNat.ofNat, Eq, LT.lt, Not, Or, Classical.em, Eq.mpr, Nat.gcd, id, congrArg, propext, Nat.coprime_iff_gcd_eq_one, Decidable.byContradiction, And and 45 more

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 54 steps

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

  8. problem Imo1971P3.imo1971_p3 line 164 source

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

    Statement uses: Exists, Set, PNat, And, Set.Infinite, Set.Pairwise, Nat.Coprime, HSub.hSub, Nat, HPow.hPow, OfNat.ofNat

    Proof uses: Exists.intro, Set.ofPred, Eq, Subtype.mk, LT.lt, Imo1971P3.a, Nat.zero_lt_of_lt, And.left, LE.le, Odd, Imo1971P3.a_ge_and_A_odd, And.intro, Set.infinite_range_of_injective, StrictMono.injective, Imo1971P3.a_strictMono, Membership.mem, Ne, Imo1971P3.a_pairwise_coprime, Eq.mpr, Set.range and 9 more

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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