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 : ℝ) : Prop

Equations

• Imo1959Q2.IsGood x A = (√(x + √(2 * x - 1)) + √(x - √(2 * x - 1)) = A ∧ 0 ≤ 2 * x - 1 ∧ 0 ≤ x + √(2 * x - 1) ∧ 0 ≤ x - √(2 * x - 1))

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.sqrt_two_mul_sub_one_le_one {x : ℝ} : √(2 * x - 1) ≤ 1 ↔ x ≤ 1

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_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.eq_sqrt_two_iff_le_one {x A : ℝ} (h : Imo1959Q2.IsGood x A) : A = √2 ↔ x ≤ 1

theorem Imo1959Q2.IsGood.sqrt_two_lt_iff_one_lt {x A : ℝ} (h : Imo1959Q2.IsGood x A) : √2 < A ↔ 1 < x

theorem Imo1959Q2.IsGood.sqrt_two_le {x A : ℝ} (h : Imo1959Q2.IsGood x A) : √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

theorem Imo1959Q2.isGood_sqrt2_iff {x : ℝ} : Imo1959Q2.IsGood x √2 ↔ x ∈ Set.Icc (1 / 2) 1

theorem Imo1959Q2.not_isGood_one {x : ℝ} : ¬Imo1959Q2.IsGood x 1

theorem Imo1959Q2.isGood_two_iff {x : ℝ} : Imo1959Q2.IsGood x 2 ↔ x = 3 / 2