Compfiles/Imo1969P2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1969, Problem 2

Let a₁, a₂, ..., aₙ be real constants, x be a real variable, and

f(x) = cos(a₁ + x) + (1/2)cos(a₂ + x) + (1/4)cos(a₃ + x) + ...

Given that f(x₁) = f(x₂) = 0 for some x₁, x₂, prove that x₂ - x₁ = mπ for some integer m.

Imports (3)
Imported by 1 file
  1. problem Imo1969P2.imo1969_p2 line 38 source

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

    Statement uses: Real, Nat, Eq, Finset.sum, Finset.range, HDiv.hDiv, Real.cos, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Ne, Exists, Int, HSub.hSub, HMul.hMul, Real.pi

    Proof uses: Real.sin, rfl, Eq.mpr, id, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Real.cos_add, Inv.inv, congr, Eq.trans, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.Common.sub_congr and 133 more

    170 instances, coercions and auxiliary constants left out.

    Tactic trace: 112 steps

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