lean_workbook_plus_20697

Proved

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

Given $A + C = 2B$ , prove the statement $\frac{1}{\sqrt{A}+\sqrt{B}}+\frac{1}{\sqrt{B}+\sqrt{C}}=\frac{2}{\sqrt{A}+\sqrt{C}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20697  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a + c = 2 * b) :
  1 / (Real.sqrt a + Real.sqrt b) + 1 / (Real.sqrt b + Real.sqrt c) =
    2 / (Real.sqrt a + Real.sqrt c)   :=  by sorry

Source

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

View graph