Compfiles/Usa1989P5.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1989, Problem 5

Let u and v be real numbers such that

(u + u² + u³ + ⋯ + u⁸) + 10u⁹ = (v + v² + v³ + ⋯ + v¹⁰) + 10v¹¹ = 8.

Determine, with proof, which of the two numbers, u or v, is larger.

Imports (2)
Imported by 1 file
  1. determine Usa1989P5.u_is_larger line 29 source

    no axioms what this means

    Statement uses: Bool

    Proof uses: Bool.false

  2. problem Usa1989P5.usa1989_p5 line 31 source

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

    Statement uses: Real, Eq, HAdd.hAdd, Finset.sum, Nat, Finset.range, OfNat.ofNat, HPow.hPow, HMul.hMul, ite, Bool, Usa1989P5.u_is_larger, Bool.true, LT.lt

    Proof uses: id, Bool.false, Ne, HDiv.hDiv, HSub.hSub, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Inv.inv, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.div_congr and 165 more

    179 instances, coercions and auxiliary constants left out.

    Tactic trace: 102 steps

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