Compfiles/Usa2001P3.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2001, Problem 3

Let a,b,c ≥ 0 be real numbers satsifying

a² + b² + c² + abc = 4.

Show that

0 ≤ ab + bc + ca - abc ≤ 2.

Imports (2)
Imported by 1 file
  1. def Usa2001P3.f line 34 source

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

    Statement uses: Real

    Proof uses: HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul

    9 instances, coercions and auxiliary constants left out.

  2. def Usa2001P3.g line 36 source

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

    Statement uses: Real

    Proof uses: HSub.hSub, HAdd.hAdd, HMul.hMul

    6 instances, coercions and auxiliary constants left out.

  3. theorem Usa2001P3.feq line 38 source

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

    Statement uses: Real, Eq, Usa2001P3.f, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul

    Proof uses: rfl

    9 instances, coercions and auxiliary constants left out.

  4. theorem Usa2001P3.geq line 39 source

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

    Statement uses: Real, Eq, Usa2001P3.g, HSub.hSub, HAdd.hAdd, HMul.hMul

    Proof uses: rfl

    6 instances, coercions and auxiliary constants left out.

  5. lemma Usa2001P3.usa2001_p3_lemma line 41 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, Nat, HMul.hMul, GE.ge, HSub.hSub

    Proof uses: Trans.trans, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 80 more

    114 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  6. problem Usa2001P3.usa2001_p3 line 62 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, Nat, HMul.hMul, And, HSub.hSub

    Proof uses: Eq.mpr, Usa2001P3.g, id, congrArg, Eq.symm, Usa2001P3.geq, Not, Or, Classical.em, Usa2001P3.f, And.intro, GE.ge, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 95 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 64 steps

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