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.
theorem
Imo1959Q2.isGood_iff_eq_sqrt_two
{x : ℝ}
{A : ℝ}
(hx : x ∈ Set.Icc (1 / 2) 1)
:
Imo1959Q2.IsGood x A ↔ A = √2
theorem
Imo1959Q2.IsGood.sqrt_two_lt_of_one_lt
{x : ℝ}
{A : ℝ}
(h : Imo1959Q2.IsGood x A)
(hx : 1 < x)
: