Polygons and quadrilaterals

Theorems about quadrilaterals, cyclic polygons and squares erected on polygon sides.

• Finsler–Hadwiger theorem
• Van Aubel's theorem

TheoremBrahmagupta's formula#✓fully proved

Let \(P, Q, R, S\) be points of the Euclidean plane with side lengths \(|PQ| = a\), \(|QR| = b\), \(|RS| = c\), \(|SP| = d\) and diagonal \(|PR| = e\), and let \(s = (a + b + c + d)/2\). Suppose that some point \(O\) is equidistant from \(P, Q, R, S\) (so the quadrilateral \(PQRS\) is cyclic) and that some point \(T\) satisfies \(|PT| + |TR| = |PR|\) and \(|QT| + |TS| = |QS|\) with \(|PT|, |TR|, |QT|, |TS| > 0\) (so \(T\) lies strictly inside both diagonals and \(PQRS\) is convex). Let \(p = (a + b + e)/2\) and \(q = (c + d + e)/2\), and let \(A\) be the sum of the Heron areas of the triangles \(PQR\) and \(RSP\):

\[A = \sqrt{p(p - a)(p - b)(p - e)} + \sqrt{q(q - c)(q - d)(q - e)}.\]

Then \(A = \sqrt{(s - a)(s - b)(s - c)(s - d)}\).

MetaMathlibExt.brahmagupta_area · 15 lines

theorem brahmagupta_area (a b c d s A e : ℝ)
    (P Q R S : EuclideanSpace ℝ (Fin 2))
    (h_sides : dist P Q = a ∧ dist Q R = b ∧ dist R S = c ∧ dist S P = d)
    (h_diag : dist P R = e)
    (h_semi : s = (a + b + c + d) / 2)
    (h_cyclic : ∃ O : EuclideanSpace ℝ (Fin 2),
      dist O P = dist O Q ∧ dist O Q = dist O R ∧ dist O R = dist O S)
    (h_convex : ∃ T : EuclideanSpace ℝ (Fin 2),
      dist P T + dist T R = dist P R ∧ dist Q T + dist T S = dist Q S ∧
      0 < dist P T ∧ 0 < dist T R ∧ 0 < dist Q T ∧ 0 < dist T S)
    (h_area : A = Real.sqrt (((a + b + e) / 2) * (((a + b + e) / 2) - a) *
        (((a + b + e) / 2) - b) * (((a + b + e) / 2) - e)) +
      Real.sqrt (((c + d + e) / 2) * (((c + d + e) / 2) - c) *
        (((c + d + e) / 2) - d) * (((c + d + e) / 2) - e)))
    : A = Real.sqrt ((s - a) * (s - b) * (s - c) * (s - d))

Sources

• https://en.wikipedia.org/wiki/Brahmagupta%27s_formula

TheoremEuler's quadrilateral theorem#✓fully proved

For any four points \(A, B, C, D\) of the Euclidean plane, write \(XY\) for the distance between points \(X\) and \(Y\), and let \(M\) and \(N\) be the midpoints of \(AC\) and \(BD\). Then

\[AB^2 + BC^2 + CD^2 + DA^2 = AC^2 + BD^2 + 4 MN^2.\]

theorem MetaMathlibExt.euler_quadrilateral {A B C D : EuclideanSpace ℝ (Fin 2)} :
    dist A B ^ 2 + dist B C ^ 2 + dist C D ^ 2 + dist D A ^ 2 =
      dist A C ^ 2 + dist B D ^ 2 +
        4 * dist ((2 : ℝ)⁻¹ • (A + C)) ((2 : ℝ)⁻¹ • (B + D)) ^ 2

Sources

• https://en.wikipedia.org/wiki/Euler%27s_quadrilateral_theorem

TheoremJapanese theorem for concyclic quadrilaterals#✓fully proved

Let \(A, B, C, D\) be pairwise distinct points of the Euclidean plane \(\mathbb{R}^2\) lying on a circle of positive radius, such that the diagonals \(AC\) and \(BD\), as closed segments, intersect; so \(ABCD\) is a convex cyclic quadrilateral. Let \(r_1, r_2, r_3, r_4 > 0\), and suppose that for each of the triangles \(ABC\), \(CDA\), \(BCD\) and \(DAB\) there is a closed disc of radius \(r_1\), \(r_2\), \(r_3\) and \(r_4\) respectively that is contained in the closed triangle and whose boundary circle meets each of the three closed sides of the triangle; so \(r_1, r_2\) are the inradii of the triangles \(ABC\), \(CDA\) of one triangulation and \(r_3, r_4\) those of the triangles \(BCD\), \(DAB\) of the other. Then \(r_1 + r_2 = r_3 + r_4\).

MetaMathlibExt.japanese_theorem_concyclic_quadrilaterals · 29 lines

theorem japanese_theorem_concyclic_quadrilaterals :
    ∀ (A B C D : EuclideanSpace ℝ (Fin 2)) (r1 r2 r3 r4 : ℝ),
      (∃ O : EuclideanSpace ℝ (Fin 2), ∃ R : ℝ, 0 < R ∧
        A ∈ Metric.sphere O R ∧ B ∈ Metric.sphere O R ∧
        C ∈ Metric.sphere O R ∧ D ∈ Metric.sphere O R) →
      (segment ℝ A C ∩ segment ℝ B D).Nonempty →
      A ≠ B → B ≠ C → C ≠ D → D ≠ A → A ≠ C → B ≠ D →
      0 < r1 → 0 < r2 → 0 < r3 → 0 < r4 →
      (∃ I1 : EuclideanSpace ℝ (Fin 2),
        Metric.closedBall I1 r1 ⊆ convexHull ℝ {A, B, C} ∧
        (segment ℝ A B ∩ Metric.sphere I1 r1).Nonempty ∧
        (segment ℝ B C ∩ Metric.sphere I1 r1).Nonempty ∧
        (segment ℝ C A ∩ Metric.sphere I1 r1).Nonempty) →
      (∃ I2 : EuclideanSpace ℝ (Fin 2),
        Metric.closedBall I2 r2 ⊆ convexHull ℝ {C, D, A} ∧
        (segment ℝ C D ∩ Metric.sphere I2 r2).Nonempty ∧
        (segment ℝ D A ∩ Metric.sphere I2 r2).Nonempty ∧
        (segment ℝ A C ∩ Metric.sphere I2 r2).Nonempty) →
      (∃ I3 : EuclideanSpace ℝ (Fin 2),
        Metric.closedBall I3 r3 ⊆ convexHull ℝ {B, C, D} ∧
        (segment ℝ B C ∩ Metric.sphere I3 r3).Nonempty ∧
        (segment ℝ C D ∩ Metric.sphere I3 r3).Nonempty ∧
        (segment ℝ D B ∩ Metric.sphere I3 r3).Nonempty) →
      (∃ I4 : EuclideanSpace ℝ (Fin 2),
        Metric.closedBall I4 r4 ⊆ convexHull ℝ {D, A, B} ∧
        (segment ℝ D A ∩ Metric.sphere I4 r4).Nonempty ∧
        (segment ℝ A B ∩ Metric.sphere I4 r4).Nonempty ∧
        (segment ℝ B D ∩ Metric.sphere I4 r4).Nonempty) →
      r1 + r2 = r3 + r4

Sources

• https://en.wikipedia.org/wiki/Japanese_theorem_for_concyclic_quadrilaterals.

Uses 1

Proof usesCarnot's theorem (inradius and circumradius), general form

TheoremVarignon's theorem#✓fully proved

Let \(A\), \(B\), \(C\), \(D\) be any four points of the Euclidean plane \(\mathbb{R}^2\), degenerate and self-crossing configurations included, and let \(P\), \(Q\), \(R\), \(S\) be the midpoints of \(AB\), \(BC\), \(CD\), \(DA\), that is \(2P = A + B\), \(2Q = B + C\), \(2R = C + D\) and \(2S = D + A\). Write \([XYZ]\) for the oriented area of the triangle \(XYZ\), positive when \(X\), \(Y\), \(Z\) are listed counterclockwise. Then \(P + R = Q + S\), so the diagonals of \(PQRS\) bisect each other and \(PQRS\) is a possibly degenerate parallelogram, and

\[2([PQR] + [PRS]) = [ABC] + [ACD],\]

that is, the signed area of \(PQRS\) is half the signed area of \(ABCD\).

theorem varignon :
  ∀ (A B C D P Q R S : EuclideanSpace ℝ (Fin 2)),
    2 • P = A + B → 2 • Q = B + C → 2 • R = C + D → 2 • S = D + A →
    P + R = Q + S ∧
    2 * (EuclideanGeometry.orientedTriangleArea P Q R +
      EuclideanGeometry.orientedTriangleArea P R S) =
      EuclideanGeometry.orientedTriangleArea A B C +
        EuclideanGeometry.orientedTriangleArea A C D

Sources

• https://en.wikipedia.org/wiki/Varignon%27s_theorem. A B C D are arbitrary points in the Euclidean plane, including degenerate or self-crossing configurations. P Q R S are the midpoints of sides AB, BC, CD, DA (2 • P = A + B, etc.). Conclusion: P + R = Q + S (the diagonals of PQRS bisect each other, i.e. PQRS is a parallelogram via parallel opposite sides / bisecting diagonals), and twice the signed area of PQRS, expressed through EuclideanGeometry.orientedTriangleArea, equals the signed area of ABCD.

Uses 1

Statement usesOriented triangle area

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.