Prove2Me

lean_workbook_plus_15538

Proved

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

(mx−b)2+(my−c)2=(nx−b)2+(ny−c)2  ⟺  (mx−nx)(mx+nx−2b)+(my−ny)(my+ny−2c)=0(m_x-b)^2+(m_y-c)^2=(n_x-b)^2+(n_y-c)^2\iff (m_x-n_x)(m_x+n_x-2b)+(m_y-n_y)(m_y+n_y-2c)=0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15538  (b c m_x m_y n_x n_y: ℝ) :
  (m_x - b)^2 + (m_y - c)^2 = (n_x - b)^2 + (n_y - c)^2 ↔ (m_x - n_x) * (m_x + n_x - 2 * b) + (m_y - n_y) * (m_y + n_y - 2 * c) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph