Documentation

Archive.Imo.Imo1960Q2

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)) ^ 2 < 2 * x + 9 0 2 * x + 1 (1 - (2 * x + 1)) ^ 2 0
structure Imo1960Q2.IsGood (x : ) :

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)) ^ 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)) ^ 2 0

    The number belongs to the domain of the denominator.

Instances For
    theorem Imo1960Q2.IsGood.ineq {x : } (self : Imo1960Q2.IsGood x) :
    4 * x ^ 2 / (1 - (2 * x + 1)) ^ 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)) ^ 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.