Erdős–Mordell inequality

DefinitionStatement of the Erdős–Mordell inequality#✓fully proved

Writing \(XY\) for the distance between points \(X\) and \(Y\), this is the assertion that for all affinely independent points \(A\), \(B\), \(C\) of the Euclidean plane, every point \(P\) in the interior of the triangle \(ABC\), and all points \(M\), \(N\), \(L\) on the lines \(BC\), \(AB\), \(CA\) such that the lines \(PM\), \(PN\), \(PL\) are perpendicular to \(BC\), \(AB\), \(CA\) respectively, we have \(PA + PB + PC \ge 2(PM + PN + PL)\).

def conjecture : Prop :=
  ∀ (A B C P L M N : ℝ²) (_hABC : AffineIndependent ℝ ![A, B, C])
    (_hP : P ∈ interior (convexHull ℝ ({A, B, C} : Set ℝ²)))
    (_hN : N ∈ line[ℝ, A, B])
    (_hPN : line[ℝ, P, N].direction ⟂ line[ℝ, A, B].direction)
    (_hM : M ∈ line[ℝ, B, C])
    (_hPM : line[ℝ, P, M].direction ⟂ line[ℝ, B, C].direction)
    (_hL : L ∈ line[ℝ, C, A])
    (_hPL : line[ℝ, P, L].direction ⟂ line[ℝ, C, A].direction),
    dist P A + dist P B + dist P C ≥ 2 * (dist P M + dist P N + dist P L)

Used by 1

Used byErdős–Mordell inequality

TheoremErdős–Mordell inequality#●ready to prove

Let \(A\), \(B\), \(C\) be affinely independent points of the Euclidean plane and \(P\) a point in the interior of the triangle \(ABC\). Let \(M\), \(N\), \(L\) be points on the lines \(BC\), \(AB\), \(CA\) such that \(PM \perp BC\), \(PN \perp AB\) and \(PL \perp CA\). Then, writing \(XY\) for the distance between points \(X\) and \(Y\), we have \(PA + PB + PC \ge 2(PM + PN + PL)\).

public theorem_wanted conjecture_holds : conjecture

Sources

• Paul Erdős, L. J. Mordell, and David F. Barrow, Problem 3740, American Mathematical Monthly 44 (1937), 252–254, https://doi.org/10.2307/2300713.

Uses 1

Statement usesStatement of the Erdős–Mordell inequality

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.