Documentation

Archive.Imo.Imo1959Q2

IMO 1959 Q2 #

For what real values of $x$ is

$\sqrt{x+\sqrt{2x-1}} + \sqrt{x-\sqrt{2x-1}} = A,$

given (a) $A=\sqrt{2}$, (b) $A=1$, (c) $A=2$, where only non-negative real numbers are admitted for square roots?

We encode the equation as a predicate saying both that the equation holds and that all arguments of square roots are nonnegative.

Then we follow second solution from the Art of Problem Solving website. Namely, we rewrite the equation as $\sqrt{2x-1}+1+|\sqrt{2x-1}-1|=A\sqrt{2}$, then consider the cases $\sqrt{2x-1}\le 1$ and $1 < \sqrt{2x-1}$ separately.

def Imo1959Q2.IsGood (x : ) (A : ) :
Equations
Instances For
    theorem Imo1959Q2.isGood_iff {x : } {A : } :
    Imo1959Q2.IsGood x A (2 * x - 1) + 1 + |(2 * x - 1) - 1| = A * 2 1 / 2 x
    theorem Imo1959Q2.IsGood.one_half_le {x : } {A : } (h : Imo1959Q2.IsGood x A) :
    1 / 2 x
    theorem Imo1959Q2.isGood_iff_eq_sqrt_two {x : } {A : } (hx : x Set.Icc (1 / 2) 1) :
    theorem Imo1959Q2.isGood_iff_eq_sqrt {x : } {A : } (hx : 1 < x) :
    Imo1959Q2.IsGood x A A = (4 * x - 2)
    theorem Imo1959Q2.IsGood.sqrt_two_lt_of_one_lt {x : } {A : } (h : Imo1959Q2.IsGood x A) (hx : 1 < x) :
    2 < A
    theorem Imo1959Q2.isGood_iff_of_sqrt_two_lt {x : } {A : } (hA : 2 < A) :
    Imo1959Q2.IsGood x A x = (A / 2) ^ 2 + 1 / 2