Compfiles/Usa1982P4.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1982, Problem 4

Prove that there exists a positive integer k such that k⬝2ⁿ + 1 is composite for every integer n.

Imports (2)
Imported by 1 file
  1. lemma Usa1982P4.not_prime_of_dvd line 28 source

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

    Statement uses: Nat, GE.ge, OfNat.ofNat, Exists, And, Ne, Dvd.dvd, Not, Prime

    Proof uses: LT.lt, Nat.Prime, Iff.mpr, Nat.prime_iff, False, Nat.minFac, Nat.not_prime_iff_minFac_lt, lt_of_le_of_ne, Nat.le_of_dvd, LE.le, Nat.minFac_le_of_dvd, lt_of_le_of_lt

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  2. lemma Usa1982P4.some_useful_mod_lemma line 38 source

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

    Statement uses: Nat, Nat.ModEq, HPow.hPow, OfNat.ofNat

    Proof uses: LE.le, Not, Or, Classical.em, Eq.mpr, HMul.hMul, id, Eq, congrArg, of_eq_true, Eq.trans, True, one_mul, eq_self, HAdd.hAdd, HSub.hSub, Iff.mp, Nat.sub_eq_iff_eq_add, rfl, pow_add and 18 more

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  3. lemma Usa1982P4.usa1982_p4_lemma line 59 source

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

    Statement uses: Nat, Or, Eq, Prod, Prod.mk, OfNat.ofNat, Nat.ModEq, Not, Prime, HAdd.hAdd, HMul.hMul, HPow.hPow

    Proof uses: HEq, eq_of_heq, Usa1982P4.not_prime_of_dvd, Nat.succ_le_succ, Trans.simple, LE.le, Eq.mpr, id, congrArg, one_mul, Nat.one_le_two_pow, mul_le_mul', of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, le_refl, Exists.intro, And and 15 more

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

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

  4. lemma Usa1982P4.usa1982_mod_lemma line 96 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, HMod.hMod, OfNat.ofNat, HMul.hMul, Nat.ModEq

    Proof uses: Nat.ModEq.trans, Eq.mpr, id, congrArg, Nat.ModEq.eq_1, Eq.symm, Nat.mod_mul_left_mod, Eq.refl

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  5. problem Usa1982P4.usa1982_p4 line 104 source

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

    Statement uses: Exists, Nat, And, LT.lt, OfNat.ofNat, Not, Prime, HAdd.hAdd, HMul.hMul, HPow.hPow

    Proof uses: Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, HMod.hMod, Eq, rfl, Eq.mpr, id, congrArg, Nat.mod_lt, Usa1982P4.usa1982_p4_lemma, of_decide_eq_true, Or, Prod, Prod.mk, Decidable.decide and 4 more

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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