Compfiles/Imo2001P6.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2001, Problem 6

Let a, b, c, d be integers with a > b > c > d > 0. Suppose that

ac + bd = (a + b - c + d) * (-a + b + c + d).

Prove that ab + cd is not prime.

Imports (2)
Imported by 1 file
  1. problem Imo2001P6.imo2001_p6 line 33 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, HSub.hSub, Neg.neg, Not, Prime

    Proof uses: Dvd.dvd, Exists.intro, HPow.hPow, Nat, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.mul_const_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 69 more

    111 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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