IMO 1960 Q2

For what values of the variable $x$ does the following inequality hold:

[\dfrac{4x^2}{(1 - \sqrt {2x + 1})^2} < 2x + 9 \ ?]

We follow solution at Art of Problem Solving with minor modifications.

theorem Imo1960Q2.isGood_iff' (x : ℝ) : Imo1960Q2.IsGood x ↔ 4 * x ^ 2 / (1 - (2 * x + 1).sqrt) ^ 2 < 2 * x + 9 ∧ 0 ≤ 2 * x + 1 ∧ (1 - (2 * x + 1).sqrt) ^ 2 ≠ 0

structure Imo1960Q2.IsGood (x : ℝ) : Prop

The predicate says that x satisfies the inequality

[\dfrac{4x^2}{(1 - \sqrt {2x + 1})^2} < 2x + 9]

and belongs to the domain of the function on the left-hand side.

• ineq : 4 * x ^ 2 / (1 - (2 * x + 1).sqrt) ^ 2 < 2 * x + 9

  The number satisfies the inequality.

• sqrt_dom : 0 ≤ 2 * x + 1

  The number belongs to the domain of (\sqrt {2x + 1}).

• denom_dom : (1 - (2 * x + 1).sqrt) ^ 2 ≠ 0

  The number belongs to the domain of the denominator.

theorem Imo1960Q2.IsGood.ineq {x : ℝ} (self : Imo1960Q2.IsGood x) : 4 * x ^ 2 / (1 - (2 * x + 1).sqrt) ^ 2 < 2 * x + 9

The number satisfies the inequality.

theorem Imo1960Q2.IsGood.sqrt_dom {x : ℝ} (self : Imo1960Q2.IsGood x) : 0 ≤ 2 * x + 1

The number belongs to the domain of (\sqrt {2x + 1}).

theorem Imo1960Q2.IsGood.denom_dom {x : ℝ} (self : Imo1960Q2.IsGood x) : (1 - (2 * x + 1).sqrt) ^ 2 ≠ 0

The number belongs to the domain of the denominator.

theorem Imo1960Q2.isGood_iff {x : ℝ} : Imo1960Q2.IsGood x ↔ x ∈ Set.Ico (-1 / 2) (45 / 8) \ {0}

Solution of IMO 1960 Q2: solutions of the inequality are the numbers of the half-closed interval ([-1/2, 45/8)) except for the number zero.