IMO 1977 LL CZS6

Origin: CZS

Problem

Let x1, x2, . . . , xn (n \geq1) be real numbers such that 0 \leqxj \leq\pi, j = 1, 2, . . ., n. Prove that if n j=1(cos xj + 1) is an odd integer, then n j=1 sin xj \geq1.

Solution

Let ⟨y⟩denote the distance from y \inR to the closest even integer. We claim that ⟨1 + cos x⟩\leqsin x for all x \in[0, \pi]. Indeed, if cos x \geq0, then ⟨1 + cos x⟩= 1 −cos x \leq1 −cos2 x = sin2 x \leq sin x; the proof is similar if cos x < 0. We note that ⟨x + y⟩\leq⟨x⟩+ ⟨y⟩holds for all x, y \inR. Therefore n  j=1 sin xj \geq n  j=1 ⟨1 + cos xj⟩\geq

n  j=1 (1 + cos xj) ? = 1.