Angle bisector theorem

TheoremAngle bisector theorem without distinctness hypotheses#✓fully proved

Let \(A\), \(B\), \(C\), \(D\) be points of a Euclidean affine space (a metric affine space over a real inner product space) with \(A\), \(B\), \(C\) affinely independent, so that \(ABC\) is a nondegenerate triangle. If \(D\) lies strictly between \(B\) and \(C\) and \(\angle BAD = \angle DAC\) (unoriented angles), then \(BD / DC = AB / AC\).

The hypotheses \(A \ne B\), \(A \ne C\) and \(A \ne D\) of the usual statement are not needed: they follow from the others.

theorem angle_bisector_theorem_general {V P : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
    [NormedAddTorsor V P]
    (A B C D : P)
    (h_tri : AffineIndependent ℝ
      (fun i : Fin 3 => if i = 0 then A else if i = 1 then B else C))
    (h_bet : Sbtw ℝ B D C)
    (h_bis : EuclideanGeometry.angle B A D = EuclideanGeometry.angle D A C) :
    dist B D / dist D C = dist A B / dist A C

Used by 1

Used byAngle bisector theorem

TheoremAngle bisector theorem#✓fully proved

Let \(A\), \(B\), \(C\), \(D\) be points of a Euclidean affine space (a metric affine space over a real inner product space) with \(A\), \(B\), \(C\) affinely independent, so that \(ABC\) is a nondegenerate triangle, and with \(A \ne B\), \(A \ne C\) and \(A \ne D\). If \(D\) lies strictly between \(B\) and \(C\) and \(\angle BAD = \angle DAC\) (unoriented angles), then \(BD / DC = AB / AC\).

@[nolint unusedArguments]
theorem angle_bisector_theorem {V P : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
    [NormedAddTorsor V P]
    (A B C D : P)
    (h_tri : AffineIndependent ℝ
      (fun i : Fin 3 => if i = 0 then A else if i = 1 then B else C))
    (hAB : A ≠ B) (hAC : A ≠ C) (hAD : A ≠ D)
    (h_bet : Sbtw ℝ B D C)
    (h_bis : EuclideanGeometry.angle B A D = EuclideanGeometry.angle D A C) :
    dist B D / dist D C = dist A B / dist A C

Sources

• https://en.wikipedia.org/wiki/Angle_bisector_theorem. It follows from angle_bisector_theorem_general; the hypotheses hAB, hAC and hAD are unused and keep the source's shape.

Uses 1

Proof usesAngle bisector theorem without distinctness hypotheses

TheoremConverse of the angle bisector theorem without distinctness hypotheses#✓fully proved

Let \(A\), \(B\), \(C\), \(D\) be points of a Euclidean affine space (a metric affine space over a real inner product space) with \(A\), \(B\), \(C\) affinely independent, so that \(ABC\) is a nondegenerate triangle. If \(D\) lies on the closed segment \(BC\) and \(BD / DC = AB / AC\), then \(\angle BAD = \angle DAC\) (unoriented angles), that is, \(D\) lies on the internal bisector of the angle at \(A\).

The hypotheses \(A \ne B\), \(A \ne C\) and \(A \ne D\) of the usual statement are not needed: they follow from the others.

theorem angle_bisector_converse_general {V P : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
    [NormedAddTorsor V P]
    (A B C D : P)
    (h_tri : AffineIndependent ℝ
      (fun i : Fin 3 => if i = 0 then A else if i = 1 then B else C))
    (h_bet : Wbtw ℝ B D C)
    (h_ratio : dist B D / dist D C = dist A B / dist A C) :
    EuclideanGeometry.angle B A D = EuclideanGeometry.angle D A C

Used by 1

Used byConverse of the angle bisector theorem

TheoremConverse of the angle bisector theorem#✓fully proved

Let \(A\), \(B\), \(C\), \(D\) be points of a Euclidean affine space (a metric affine space over a real inner product space) with \(A\), \(B\), \(C\) affinely independent, so that \(ABC\) is a nondegenerate triangle, and with \(A \ne B\), \(A \ne C\) and \(A \ne D\). If \(D\) lies on the closed segment \(BC\) and \(BD / DC = AB / AC\), then \(\angle BAD = \angle DAC\) (unoriented angles), that is, \(D\) lies on the internal bisector of the angle at \(A\).

@[nolint unusedArguments]
theorem angle_bisector_converse {V P : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
    [NormedAddTorsor V P]
    (A B C D : P)
    (h_tri : AffineIndependent ℝ
      (fun i : Fin 3 => if i = 0 then A else if i = 1 then B else C))
    (hAB : A ≠ B) (hAC : A ≠ C) (hAD : A ≠ D)
    (h_bet : Wbtw ℝ B D C)
    (h_ratio : dist B D / dist D C = dist A B / dist A C) :
    EuclideanGeometry.angle B A D = EuclideanGeometry.angle D A C

Sources

• https://en.wikipedia.org/wiki/Angle_bisector_theorem. It follows from angle_bisector_converse_general; the hypotheses hAB, hAC and hAD are unused and keep the source's shape.

Uses 1

Proof usesConverse of the angle bisector theorem without distinctness hypotheses

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.