Van Schooten's theorem

TheoremVan Schooten's theorem#✓fully proved

Let \(A\), \(B\), \(C\), \(P\) and \(O\) be points of the Euclidean plane \(\mathbb{R}^2\) and let \(r > 0\). Suppose that \(AB = BC = CA\), that \(A\), \(B\), \(C\) and \(P\) lie on the circle of radius \(r\) about \(O\), and that \(CP > AP\) and \(CP > BP\). Then \(PA + PB = PC\).

No hypothesis that \(P\) differs from \(A\), \(B\) or \(C\) is needed.

theorem vanSchooten_general (A B C P O : EuclideanSpace ℝ (Fin 2)) (r : ℝ) (hr : 0 < r)
    (he1 : dist A B = dist B C) (he2 : dist B C = dist C A)
    (hA : A ∈ Metric.sphere O r) (hB : B ∈ Metric.sphere O r)
    (hC : C ∈ Metric.sphere O r) (hP : P ∈ Metric.sphere O r)
    (h1 : dist C P > dist A P) (h2 : dist C P > dist B P) :
    dist P A + dist P B = dist P C

Used by 1

Used byVan Schooten's theorem with distinctness hypotheses

TheoremVan Schooten's theorem with distinctness hypotheses#✓fully proved

Let \(A\), \(B\), \(C\), \(P\) and \(O\) be points of the Euclidean plane \(\mathbb{R}^2\) and let \(r > 0\). Suppose that \(AB = BC = CA\), that \(A\), \(B\), \(C\) and \(P\) lie on the circle of radius \(r\) about \(O\), that \(P \ne A\), \(P \ne B\) and \(P \ne C\), and that \(CP > AP\) and \(CP > BP\). Then \(PA + PB = PC\).

In the source, \(P\) is a point on the arc \(AB\) of the circumcircle not containing \(C\); here that condition is expressed by \(CP > AP\) and \(CP > BP\).

theorem vanSchooten : ∀ (A B C P O : EuclideanSpace ℝ (Fin 2)) (r : ℝ),
  0 < r →
  dist A B = dist B C →
  dist B C = dist C A →
  A ∈ Metric.sphere O r →
  B ∈ Metric.sphere O r →
  C ∈ Metric.sphere O r →
  P ∈ Metric.sphere O r →
  P ≠ A → P ≠ B → P ≠ C →
  dist C P > dist A P →
  dist C P > dist B P →
  dist P A + dist P B = dist P C

Sources

• https://en.wikipedia.org/wiki/Van_Schooten%27s_theorem. It follows from vanSchooten_general; the hypotheses P ≠ A, P ≠ B and P ≠ C are unused and keep the source's shape.

Uses 1

Proof usesVan Schooten's theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.