Prove2Me

lean_workbook_plus_16642

Proved

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

Let a,b,c>0a,b,c>0 and a+b+c>1a+b+c>1 . Prove that \n

1a+b+c−1+b+ca+c+ab+a+bc≥2+1a+1b+1c\frac{1}{a+b+c-1}+\frac{b+c}{a} +\frac{c+a}{b}+\frac{a+b}{c}\ge 2+\frac{1}{a}+\frac{1}{b}+\frac{1}{c}

\n

  ⟺  1a+b+c−1+(a+b+c−1)(1a+1b+1c)≥5\iff \frac{1}{a+b+c-1}+(a+b+c-1)\left(\frac{1}{a}+\frac{1}{b}+\frac{1}{c}\right)\ge 5
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16642 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (habc : a * b * c = 1) : 1 / (a + b + c - 1) + (b + c) / a + (c + a) / b + (a + b) / c ≥ 2 + 1 / a + 1 / b + 1 / c ↔ 1 / (a + b + c - 1) + (a + b + c - 1) * (1 / a + 1 / b + 1 / c) ≥ 5   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph