Morley's trisector theorem

AbbreviationEuclidean plane for Morley's theorem#✓fully proved

The Euclidean plane \(\mathbb{R}^2\) with its standard Euclidean distance.

abbrev Plane := EuclideanSpace ℝ (Fin 2)

Used by 4

Used byEquilateral triple of points · Morley configuration · Point in a closed triangle · Morley's trisector theorem

DefinitionEquilateral triple of points#✓fully proved

Three points \(P\), \(Q\), \(R\) of the Euclidean plane form an equilateral triple when, writing \(d\) for the Euclidean distance, \(d(P, Q) = d(Q, R)\) and \(d(Q, R) = d(R, P)\). Coincident points are allowed, so \(P = Q = R\) qualifies.

def IsEquilateralTriple (P Q R : Plane) : Prop :=
  dist P Q = dist Q R ∧ dist Q R = dist R P

Uses 1 · Used by 1

Statement usesEuclidean plane for Morley's theorem

Used byMorley's trisector theorem

DefinitionPoint in a closed triangle#✓fully proved

A point \(X\) of the Euclidean plane lies in the triangle with vertices \(A\), \(B\), \(C\) when \(X\) belongs to the convex hull of \(\{A, B, C\}\), the closed triangle \(ABC\) (a segment or a point when \(A\), \(B\), \(C\) are collinear).

def LiesInTriangle (A B C X : Plane) : Prop :=
  X ∈ convexHull ℝ ({A, B, C} : Set Plane)

Uses 1 · Used by 1

Statement usesEuclidean plane for Morley's theorem

Used byMorley configuration

DefinitionMorley configuration#✓fully proved

Points \(A\), \(B\), \(C\), \(P\), \(Q\), \(R\) of the Euclidean plane form a Morley configuration when \(A\), \(B\), \(C\) are not collinear, each of \(P\), \(Q\), \(R\) lies in the closed triangle \(ABC\), and, writing \(\angle XYZ \in [0, \pi]\) for the unoriented angle at \(Y\), \(0 < \angle CAR = \angle RAP = \angle PAB\) and \(3 \angle PAB = \angle CAB\); \(0 < \angle ABP = \angle PBQ = \angle QBC\) and \(3 \angle QBC = \angle ABC\); \(0 < \angle BCQ = \angle QCR = \angle RCA\) and \(3 \angle RCA = \angle BCA\). Thus \(P\), \(Q\), \(R\) are the intersections of adjacent angle trisectors of the triangle \(ABC\).

def IsMorleyConfiguration (A B C P Q R : Plane) : Prop :=
  ¬ Collinear ℝ ({A, B, C} : Set Plane) ∧
  LiesInTriangle A B C P ∧ LiesInTriangle A B C Q ∧ LiesInTriangle A B C R ∧
  0 < (∠ C A R) ∧ (∠ C A R) = (∠ R A P) ∧ (∠ R A P) = (∠ P A B) ∧
  3 * (∠ P A B) = (∠ C A B) ∧
  0 < (∠ A B P) ∧ (∠ A B P) = (∠ P B Q) ∧ (∠ P B Q) = (∠ Q B C) ∧
  3 * (∠ Q B C) = (∠ A B C) ∧
  0 < (∠ B C Q) ∧ (∠ B C Q) = (∠ Q C R) ∧ (∠ Q C R) = (∠ R C A) ∧
  3 * (∠ R C A) = (∠ B C A)

Uses 2 · Used by 1

Statement usesPoint in a closed triangle · Euclidean plane for Morley's theorem

Used byMorley's trisector theorem

TheoremMorley's trisector theorem#●ready to prove

If points \(A\), \(B\), \(C\), \(P\), \(Q\), \(R\) of the Euclidean plane form a Morley configuration, so that \(ABC\) is a nondegenerate triangle and \(P\), \(Q\), \(R\) are the intersections of its adjacent angle trisectors, then \(P\), \(Q\), \(R\) form an equilateral triple: writing \(d\) for the Euclidean distance, \(d(P, Q) = d(Q, R)\) and \(d(Q, R) = d(R, P)\).

public theorem_wanted morley_theorem (A B C P Q R : Plane)
    (h : IsMorleyConfiguration A B C P Q R) :
    IsEquilateralTriple P Q R

Sources

• F. Morley (c. 1899). Knill, §162. Problem morley_theorem of the lean-eval benchmark.

Uses 3

Statement usesEquilateral triple of points · Morley configuration · Euclidean plane for Morley's theorem

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.