Prove2Me

lean_workbook_plus_11976

Proved

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

(A→−C→)2+(B→−D→)2+(A→−D→)2+(B→−C→)2≥(A→−B→)2+(C→−D→)2(\overrightarrow{A}-\overrightarrow{C})^2+(\overrightarrow{B}-\overrightarrow{D})^2+(\overrightarrow{A}-\overrightarrow{D})^2+(\overrightarrow{B}-\overrightarrow{C})^2\ge (\overrightarrow{A}-\overrightarrow{B})^2 + (\overrightarrow{C}-\overrightarrow{D})^2   ⟹  A→2+B→2+C→2+D→2−2A→C→−2B→D→−2A→D→−2B→C→+2A→B→−2C→D→≥0\implies \overrightarrow{A}^2+ \overrightarrow{B}^2+ \overrightarrow{C}^2+ \overrightarrow{D}^2 - 2\overrightarrow{A}\overrightarrow{C}- 2\overrightarrow{B}\overrightarrow{D}- 2\overrightarrow{A}\overrightarrow{D}- 2\overrightarrow{B}\overrightarrow{C}+ 2\overrightarrow{A}\overrightarrow{B}- 2\overrightarrow{C}\overrightarrow{D}\ge 0   ⟹  (A→+B→−C→−D→)2≥0.\implies (\overrightarrow{A}+\overrightarrow{B}-\overrightarrow{C}-\overrightarrow{D})^2 \ge 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11976 (A B C D : ℝ) : (A - C) ^ 2 + (B - D) ^ 2 + (A - D) ^ 2 + (B - C) ^ 2 ≥ (A - B) ^ 2 + (C - D) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph