20 lines
1.0 KiB
Plaintext
20 lines
1.0 KiB
Plaintext
|
-- {
|
|||
|
|
-- "problem": "If $\\sqrt{2\\sqrt{t-2}} = \\sqrt[4]{7 - t}$, then find $t$.",
|
|||
|
|
-- "level": "Level 4",
|
|||
|
|
-- "type": "Algebra",
|
|||
|
|
-- "solution": "We raise both sides to the fourth power, which is equivalent to squaring twice, in order to get rid of the radicals. The left-hand side becomes $$\\left(\\sqrt{2\\sqrt{t-2}}\\right)^4 = \\left(2\\sqrt{t-2}\\right)^2 = 4 \\cdot (t-2) = 4t-8.$$The right-hand side becomes $\\left(\\sqrt[4]{7-t}\\right)^4 = 7-t$. Setting them equal, $$4t-8 = 7-t \\quad\\Longrightarrow\\quad 5t = 15,$$and $t = \\boxed{3}$. Checking, we find that this value does indeed satisfy the original equation."
|
|||
|
|
-- }
|
|||
|
|
|
|||
|
|
import Mathlib.Data.Real.Basic
|
|||
|
|
import Mathlib.Data.Nat.Pow
|
|||
|
|
|
|||
|
|
noncomputable def a (t : ℝ) : ℝ := (2 * (t - 2) ^ (1 / 2)) ^ (1/2)
|
|||
|
|
noncomputable def b (t : ℝ) : ℝ := (7 - t)^(1/4)
|
|||
|
|
|
|||
|
|
def valid_t (t : ℝ) : Prop :=
|
|||
|
|
a t = b t
|
|||
|
|
|
|||
|
|
theorem LHS_to_4 : ∀ t : ℝ, (a t) ^ 4 = 4 * t - 8 := by sorry
|
|||
|
|
theorem RHS_to_4 : ∀ t : ℝ, (b t) ^ 4 = 7 - t := by sorry
|
|||
|
|
theorem solution : valid_t 3 := by sorry
|