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.

source
def Imo1959Q2.IsGood (x : ℝ) (A : ℝ) :
Prop
Equations
Instances For
    source
    theorem Imo1959Q2.isGood_iff {x : ℝ} {A : ℝ} :
    Imo1959Q2.IsGood x A ↔ (2 * x - 1).sqrt + 1 + |(2 * x - 1).sqrt - 1| = A * √2 ∧ 1 / 2 ≤ x
    source
    theorem Imo1959Q2.IsGood.one_half_le {x : ℝ} {A : ℝ} (h : Imo1959Q2.IsGood x A) :
    1 / 2 ≤ x
    source
    theorem Imo1959Q2.sqrt_two_mul_sub_one_le_one {x : ℝ} :
    (2 * x - 1).sqrt ≤ 1 ↔ x ≤ 1
    source
    theorem Imo1959Q2.isGood_iff_eq_sqrt_two {x : ℝ} {A : ℝ} (hx : x ∈ Set.Icc (1 / 2) 1) :
    Imo1959Q2.IsGood x A ↔ A = √2
    source
    theorem Imo1959Q2.isGood_iff_eq_sqrt {x : ℝ} {A : ℝ} (hx : 1 < x) :
    Imo1959Q2.IsGood x A ↔ A = (4 * x - 2).sqrt
    source
    theorem Imo1959Q2.IsGood.sqrt_two_lt_of_one_lt {x : ℝ} {A : ℝ} (h : Imo1959Q2.IsGood x A) (hx : 1 < x) :
    √2 < A
    source
    theorem Imo1959Q2.IsGood.eq_sqrt_two_iff_le_one {x : ℝ} {A : ℝ} (h : Imo1959Q2.IsGood x A) :
    A = √2 ↔ x ≤ 1
    source
    theorem Imo1959Q2.IsGood.sqrt_two_lt_iff_one_lt {x : ℝ} {A : ℝ} (h : Imo1959Q2.IsGood x A) :
    √2 < A ↔ 1 < x
    source
    theorem Imo1959Q2.IsGood.sqrt_two_le {x : ℝ} {A : ℝ} (h : Imo1959Q2.IsGood x A) :
    √2 ≤ A
    source
    theorem Imo1959Q2.isGood_iff_of_sqrt_two_lt {x : ℝ} {A : ℝ} (hA : √2 < A) :
    Imo1959Q2.IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2
    source
    theorem Imo1959Q2.isGood_sqrt2_iff {x : ℝ} :
    Imo1959Q2.IsGood x √2 ↔ x ∈ Set.Icc (1 / 2) 1
    source
    theorem Imo1959Q2.not_isGood_one {x : ℝ} :
    ¬Imo1959Q2.IsGood x 1
    source
    theorem Imo1959Q2.isGood_two_iff {x : ℝ} :
    Imo1959Q2.IsGood x 2 ↔ x = 3 / 2