Compfiles/Usa2015P5.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2015, Problem 5

Let a, b, c, d, e be distinct positive integers such that a⁴+b⁴ = c⁴+d⁴ = e⁵. Show that ac+bd is a composite number.

Imports (3)
Imported by 1 file
  1. lemma Usa2015P5.p_divis line 44 source

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

    Statement uses: Nat, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, ZMod, HMul.hMul, HSub.hSub

    Proof uses: id, congrArg, of_eq_true, Eq.trans, True, congrFun', congr, CharP.cast_eq_zero, eq_self, Eq.mp, Nat.cast_add, Nat.cast_pow

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  2. lemma Usa2015P5.e_lt_p line 52 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, HMul.hMul

    Proof uses: Trans.trans, LE.le, Eq.symm, add_le_add, Nat.pow_le_pow_right, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Eq.mpr, id, congrArg, Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Mathlib.Tactic.Ring.Common.add_pf_add_lt and 83 more

    155 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  3. lemma Usa2015P5.not_p_dvd_e line 61 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, Not, Dvd.dvd, HMul.hMul

    Proof uses: Nat.not_dvd_of_pos_of_lt, Usa2015P5.e_lt_p

    21 instances, coercions and auxiliary constants left out.

  4. lemma Usa2015P5.not_p_dvd_e_pow_5 line 65 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, Nat.Prime, HMul.hMul, Not, Dvd.dvd

    Proof uses: Usa2015P5.not_p_dvd_e, Mathlib.Tactic.Contrapose.contrapose₄, Nat.Prime.dvd_of_dvd_pow

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. lemma Usa2015P5.p_le_aa_plus_dd line 71 source

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

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

    Proof uses: Not, Or, Classical.em, Nat.lt_of_le_of_ne, id, Ne.symm, ZMod, HSub.hSub, Usa2015P5.p_divis, Dvd.dvd, Or.resolve_right, Eq.mp, congrArg, propext, Nat.Prime.dvd_mul, ZMod.natCast_eq_zero_iff, congrFun', Eq.trans, congr, AddGroupWithOne and 91 more

    142 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

  6. problem Usa2015P5.usa2015_p5 line 95 source

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

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

    Proof uses: And.intro, LE.le, Or, Classical.em, Nat.lt_of_le_of_ne, id, Usa2015P5.p_le_aa_plus_dd, pow_lt_pow_left₀, le_of_lt, ne_of_gt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, lt_of_pow_lt_pow_left', Eq.mp, congrArg, Eq.symm, False.elim and 86 more

    134 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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