← Formalpedia
lean_workbook_plus_17704 Proved by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
a 1 ∗ ( b + c 2 ) + b 1 ∗ ( c + a 2 ) + c 1 ∗ ( a + b 2 ) = a 2 ∗ ( b 1 + c ) + b 2 ∗ ( a + c 1 ) + c 2 ∗ ( b + a 1 ) a_1*(b+c_2)+ b_1*(c+a_2)+ c_1*(a+b_2)= a_2*(b_1+c)+ b_2*(a+c_1)+ c_2*(b+a_1) a 1 ∗ ( b + c 2 ) + b 1 ∗ ( c + a 2 ) + c 1 ∗ ( a + b 2 ) = a 2 ∗ ( b 1 + c ) + b 2 ∗ ( a + c 1 ) + c 2 ∗ ( b + a 1 ) a 1 b + b 1 c + c 1 a = a 2 c + b 2 a + c 2 b a_1b+b_1c+c_1a=a_2c+b_2a+c_2b a 1 b + b 1 c + c 1 a = a 2 c + b 2 a + c 2 b ( B X 2 − C X 1 ) ⋅ B C + ( C Y 2 − A Y 1 ) ⋅ C A + ( A Z 2 − B Z 1 ) ⋅ A B = 0 \left( BX_2-CX_1\right) \cdot BC+\left( CY_2-AY_1\right) \cdot CA+\left( AZ_2-BZ_1\right) \cdot AB=0 ( B X 2 − C X 1 ) ⋅ B C + ( C Y 2 − A Y 1 ) ⋅ C A + ( A Z 2 − B Z 1 ) ⋅ A B = 0
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_17704 :
∀ a b c a₂ b₂ c₂ : ℝ,
a * (b + c₂) + b * (c + a₂) + c * (a + b₂) = a₂ * (b + c) + b₂ * (c + a) + c₂ * (a + b) ↔
a * b + b * c + c * a = a₂ * c + b₂ * a + c₂ * b := by sorry View graph