Compfiles/Imo1987P6.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1987, Problem 6

Let $n$ be an integer greater than or equal to 2. Prove that if $k^2 + k + n$ is prime for all integers $k$ such that $0 <= k <= \sqrt{n/3}$, then $k^2 + k + n$ is prime for all integers $k$ such that $0 <= k <= n - 2$.

Imports (4)
Imported by 1 file
  1. lemma Imo1987P6.minFac_le_sq line 32 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Nat.minFac, LE.le, HPow.hPow

    Proof uses: absurd, Eq, Eq.refl, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.minFac_one, one_pow, HAdd.hAdd, HMul.hMul, Dvd.dvd, Nat.minFac_dvd, False.elim, Eq.mp, False, mul_one, Not, eq_self and 41 more

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  2. lemma Imo1987P6.prime_of_coprime' line 49 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HPow.hPow, Ne, Nat.Coprime, Nat.Prime

    Proof uses: Eq.mpr, And, Eq, Nat.minFac, id, congrArg, propext, Nat.prime_def_minFac, Decidable.byContradiction, Not, Eq.mp, Mathlib.Tactic.Push.not_and_eq, Nat.minFac_pos, Imo1987P6.minFac_le_sq, Iff.mpr, Exists, Dvd.dvd, Nat.Prime.not_coprime_iff_dvd, Exists.intro, of_eq_true and 6 more

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  3. lemma Imo1987P6.dyadic line 62 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Exists, And, LT.lt, HMul.hMul, HPow.hPow

    Proof uses: Ne, HDiv.hDiv, Iff.mpr, Nat.div_ne_zero_iff, Exists.intro, HAdd.hAdd, Nat.log2, And.intro, Nat.lt_succ_self, Iff.mp, Nat.log2_lt, Nat.succ, Nat.succ_le_of_lt, Trans.trans, Eq, Nat.lt_div_mul_add, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr and 29 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

  4. lemma Imo1987P6.key_lemma line 83 source

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

    Statement uses: Nat, LT.lt, LE.le, HMul.hMul, OfNat.ofNat, Nat.Coprime

    Proof uses: dite, Not, And, HPow.hPow, Exists, Imo1987P6.dyadic, le_of_lt, Eq.mp, Nat.Coprime.coprime_mul_left_right

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  5. lemma Imo1987P6.key_lemma' line 93 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, Nat.Coprime, HPow.hPow, HAdd.hAdd, Nat.Prime

    Proof uses: Imo1987P6.key_lemma, Imo1987P6.prime_of_coprime', Ne, dite, Eq, of_eq_true, Eq.trans, True, congrArg, Nat.coprime_one_right_eq_true, Not, lt_of_le_of_lt, Iff.mp, Nat.mul_self_lt_mul_self_iff, Eq.mp, pow_two

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  6. lemma Imo1987P6.dvd_lemma line 109 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, LE.le, Dvd.dvd, LT.lt, HMul.hMul, Eq

    Proof uses: False.elim, Eq.mp, congrArg, MulZeroClass.mul_zero, of_eq_true, Eq.trans, True, mul_one, eq_self, HAdd.hAdd

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  7. lemma Imo1987P6.zero_of_le_sub_pos line 116 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, LE.le, HSub.hSub, Eq

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. lemma Imo1987P6.sub_le_lemma line 118 source

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

    Statement uses: Nat, LE.le, Ne, OfNat.ofNat, LT.lt, HSub.hSub

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. problem Imo1987P6.imo1987_p6 line 122 source

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

    Statement uses: Nat, LE.le, Nat.floor, Real, Real.sqrt, HDiv.hDiv, OfNat.ofNat, Nat.Prime, HAdd.hAdd, HPow.hPow, HSub.hSub

    Proof uses: Nat.case_strong_induction_on, Nat.zero_le, dite, Not, Eq, Nat.eq_add_of_sub_eq, le_of_lt, Eq.mp, LT.lt, Eq.refl, id, Nat.le_sub_of_add_le', HMul.hMul, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 130 more

    205 instances, coercions and auxiliary constants left out.

    Tactic trace: 102 steps

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