lean_workbook_plus_27699

Proved

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

Prove that $\left\|\begin{array}{c}abc\ne 0\\a^2=b(b+c)\\b^2=c(c+a)\end{array}\right\|\ \implies\ \frac 1c=\frac 1a+\frac 1b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27699 (a b c : ℝ) (h₁ : a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0) (h₂ : a^2 = b * (b + c)) (h₃ : b^2 = c * (c + a)) : 1 / c = 1 / a + 1 / b   :=  by sorry

Source

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

View graph