Compfiles/Imo2003P6.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2003, Problem 6

Let p be a prime number. Prove that there exists a prime number q such that for every integer n, the number nᵖ - p is not divisible by q.

Imports (3)
Imported by 1 file
  1. lemma Imo2003P6.exists_prime_mod_m_ne_1_and_dvd line 30 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, HMod.hMod, Exists, And, Nat.Prime, Dvd.dvd

    Proof uses: Classical.byContradiction, Not, List, Nat.primeFactorsList, Membership.mem, Eq, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Nat.prime_of_mem_primeFactorsList, Nat.dvd_of_mem_primeFactorsList, Trans.trans, List.prod, List.map, rfl, Eq.mpr and 18 more

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  2. problem Imo2003P6.imo2003_p6 line 48 source

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

    Statement uses: Nat, Nat.Prime, Exists, And, Int, Not, Dvd.dvd, HSub.hSub, HPow.hPow

    Proof uses: Eq, OfNat.ofNat, HMod.hMod, Or, Nat.Prime.eq_two_or_odd, Exists.intro, And.intro, Nat.prime_five, id, LE.le, Int.emod_nonneg, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, LT.lt, Int.emod_lt_of_pos, Mathlib.Meta.NormNum.isNat_lt_true, Int.ModEq and 196 more

    184 instances, coercions and auxiliary constants left out.

    Tactic trace: 173 steps

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