lean_workbook_plus_27775

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $f(x)=\sqrt{x^2-2x+10}+\sqrt{x^2-16x+80}=\sqrt{(x-1)^2+3^2}+\sqrt{(x-8)^2+4^2}$ . Then, by Cauchy Schwarz Inequality, we have\n\n$f(x)^2=x^2-2x+10+x^2-16x+80+2\sqrt{[(x-1)^2+3^2][(x-8)^2+4^2]}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27775 (x : ℝ) :
  (Real.sqrt (x^2 - 2*x + 10) + Real.sqrt (x^2 - 16*x + 80))^2 ≥
  x^2 - 2*x + 10 + x^2 - 16*x + 80 + 2 * Real.sqrt ((x-1)^2 + 3^2) * Real.sqrt ((x-8)^2 + 4^2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph