Menelaus's theorem

TheoremMenelaus's theorem, general form#✓fully proved

Let \(A\), \(B\), \(C\) be points of the Euclidean plane \(\mathbb{R}^2\) with \(A \ne B\) and \(C\) not on the line \(AB\). Let \(D\), \(E\), \(F\) be points and let \(\alpha, \alpha', \beta, \beta', \gamma, \gamma'\) be real numbers with \(F - A = \alpha (B - A)\), \(B - F = \alpha' (B - A)\), \(D - B = \beta (C - B)\), \(C - D = \beta' (C - B)\), \(E - C = \gamma (A - C)\), \(A - E = \gamma' (A - C)\), and \(\alpha', \beta', \gamma' \ne 0\). Then \(F\) lies on the line through \(D\) and \(E\) if and only if \(\frac{\alpha}{\alpha'} \cdot \frac{\beta}{\beta'} \cdot \frac{\gamma}{\gamma'} = -1\).

The numbers \(\alpha, \alpha', \beta, \beta', \gamma, \gamma'\) are the signed ratios \(AF/AB\), \(FB/AB\), \(BD/BC\), \(DC/BC\), \(CE/CA\), \(EA/CA\), so the product is the classical signed ratio product \(\frac{AF}{FB} \cdot \frac{BD}{DC} \cdot \frac{CE}{EA}\).

theorem menelaus_general {A B C D E F : EuclideanSpace ℝ (Fin 2)} {AF FB BD DC CE EA : ℝ}
    (hnc : ¬ ∃ t : ℝ, AffineMap.lineMap A B t = C) (hAB : A ≠ B)
    (hFAv : F - A = AF • (B - A)) (hBFv : B - F = FB • (B - A))
    (hDBv : D - B = BD • (C - B)) (hCDv : C - D = DC • (C - B))
    (hECv : E - C = CE • (A - C)) (hAEv : A - E = EA • (A - C))
    (hFB0 : FB ≠ 0) (hDC0 : DC ≠ 0) (hEA0 : EA ≠ 0) :
    (∃ t : ℝ, AffineMap.lineMap D E t = F) ↔ (AF / FB) * (BD / DC) * (CE / EA) = -1

Used by 1

Used byMenelaus's theorem

TheoremMenelaus's theorem#✓fully proved

Let \(A\), \(B\), \(C\) be pairwise distinct points of the Euclidean plane \(\mathbb{R}^2\) with \(C\) not on the line \(AB\). Let \(D\), \(E\), \(F\) be points on the lines \(BC\), \(CA\) and \(AB\) respectively, with \(D \ne B\), \(D \ne C\), \(E \ne C\), \(E \ne A\), \(F \ne A\) and \(F \ne B\). Let \(\alpha, \alpha', \beta, \beta', \gamma, \gamma'\) be real numbers with \(F - A = \alpha (B - A)\), \(B - F = \alpha' (B - A)\), \(D - B = \beta (C - B)\), \(C - D = \beta' (C - B)\), \(E - C = \gamma (A - C)\), \(A - E = \gamma' (A - C)\), and \(\alpha', \beta', \gamma' \ne 0\). Then \(F\) lies on the line through \(D\) and \(E\) if and only if \(\frac{\alpha}{\alpha'} \cdot \frac{\beta}{\beta'} \cdot \frac{\gamma}{\gamma'} = -1\).

The numbers \(\alpha, \alpha', \beta, \beta', \gamma, \gamma'\) are the signed ratios \(AF/AB\), \(FB/AB\), \(BD/BC\), \(DC/BC\), \(CE/CA\), \(EA/CA\), so the product is the classical signed ratio product \(\frac{AF}{FB} \cdot \frac{BD}{DC} \cdot \frac{CE}{EA}\). The incidence hypotheses, \(B \ne C\), \(A \ne C\) and the conditions that \(D\), \(E\), \(F\) avoid the vertices follow from the other hypotheses or are not needed; they keep the shape of the classical statement.

MetaMathlibExt.menelaus · 16 lines

theorem menelaus :
    ∀ (A B C D E F : EuclideanSpace ℝ (Fin 2)) (AF FB BD DC CE EA : ℝ),
      (¬ ∃ t : ℝ, AffineMap.lineMap A B t = C) →
      A ≠ B → B ≠ C → A ≠ C →
      (∃ tD : ℝ, AffineMap.lineMap B C tD = D) →
      (∃ tE : ℝ, AffineMap.lineMap C A tE = E) →
      (∃ tF : ℝ, AffineMap.lineMap A B tF = F) →
      D ≠ B → D ≠ C → E ≠ C → E ≠ A → F ≠ A → F ≠ B →
      (F - A = AF • (B - A)) →
      (B - F = FB • (B - A)) →
      (D - B = BD • (C - B)) →
      (C - D = DC • (C - B)) →
      (E - C = CE • (A - C)) →
      (A - E = EA • (A - C)) →
      FB ≠ 0 → DC ≠ 0 → EA ≠ 0 →
      ((∃ t : ℝ, AffineMap.lineMap D E t = F) ↔ (AF / FB) * (BD / DC) * (CE / EA) = -1)

Sources

• https://en.wikipedia.org/wiki/Menelaus%27s_theorem.

Uses 1

Proof usesMenelaus's theorem, general form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.