← Formalpedia
lean_workbook_plus_76132 Proved by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Let a a a b b b c c c
a 3 ( b − c ) 2 + b 3 ( c − a ) 2 + c 3 ( a − b ) 2 = a + b + c + ( a b − c + b c − a + c a − b ) ( a 2 b − c + b 2 c − a + c 2 a − b ) \frac{a^3}{(b-c)^2}+ \frac{b^3}{(c-a)^2}+ \frac{c^3}{(a-b)^2}=a+b+c+\left(\frac{a}{b-c}+ \frac{b}{c-a}+ \frac{c}{a-b} \right)\left(\frac{a^2}{b-c}+ \frac{b^2}{c-a}+ \frac{c^2}{a-b} \right) ( b − c ) 2 a 3 + ( c − a ) 2 b 3 + ( a − b ) 2 c 3 = a + b + c + ( b − c a + c − a b + a − b c ) ( b − c a 2 + c − a b 2 + a − b c 2 ) \nLet a 1 , a 2 , ⋯ , a n ( n ≥ 2 ) a_1,a_2,\cdots,a_n (n\ge 2) a 1 , a 2 , ⋯ , a n ( n ≥ 2 )
a 1 3 ( a 2 − a 3 ) 2 + a 2 3 ( a 3 − a 4 ) 2 + ⋯ + a n − 1 3 ( a n − a 1 ) 2 + a n 3 ( a 1 − a 2 ) 2 ≥ a 1 + a 2 + ⋯ + a n . \frac{a^3_1}{(a_2-a_3)^2}+\frac{a^3_2}{(a_3-a_4)^2}+\cdots+\frac{a^3_{n-1}}{(a_n-a_1)^2}+\frac{a^3_n}{(a_1-a_2)^2}\geq a_1+a_2+\cdots +a_n. ( a 2 − a 3 ) 2 a 1 3 + ( a 3 − a 4 ) 2 a 2 3 + ⋯ + ( a n − a 1 ) 2 a n − 1 3 + ( a 1 − a 2 ) 2 a n 3 ≥ a 1 + a 2 + ⋯ + a n . (Jichen) p/6748080023\n\n
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_76132 (a b c : ℝ) (hab : a ≠ b) (hbc : b ≠ c) (hca : c ≠ a) : a^3 / (b - c)^2 + b^3 / (c - a)^2 + c^3 / (a - b)^2 = a + b + c + (a / (b - c) + b / (c - a) + c / (a - b)) * (a^2 / (b - c) + b^2 / (c - a) + c^2 / (a - b)) := by sorry View graph