Carnot's theorem

TheoremCarnot's theorem (inradius and circumradius), general form#✓fully proved

Let \(A, B, C\) be non-collinear points of a Euclidean affine plane lying on the circle with center \(O\) and radius \(R > 0\). Take unit vectors \(n_a\), \(n_b\), \(n_c\) normal to the sides and pointing toward the opposite vertices: \(n_a \perp C - B\) with \(\langle A - B, n_a \rangle > 0\), \(n_b \perp A - C\) with \(\langle B - C, n_b \rangle > 0\), and \(n_c \perp B - A\) with \(\langle C - A, n_c \rangle > 0\). Let \(x = \langle O - B, n_a \rangle\), \(y = \langle O - C, n_b \rangle\) and \(z = \langle O - A, n_c \rangle\) be the signed distances from \(O\) to the lines \(BC\), \(CA\), \(AB\). If a point \(I\) and a real number \(r\) satisfy \(\langle I - B, n_a \rangle = \langle I - C, n_b \rangle = \langle I - A, n_c \rangle = r\) (so \(I\) is the incenter and \(r\) the inradius), then \(x + y + z = R + r\).

This form does not assume \(r > 0\) or that \(O\) lies in the affine span of \(A, B, C\).

MetaMathlibExt.carnot_inradius_circumradius_general · 28 lines

theorem carnot_inradius_circumradius_general
    {V : Type*} {P : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [MetricSpace P] [NormedAddTorsor V P]
    [Fact (Module.finrank ℝ V = 2)]
    (A B C O I : P) (R r x y z : ℝ)
    (nBC nCA nAB : V)
    (hTri : ¬ Collinear ℝ ({A, B, C} : Set P))
    (hRpos : 0 < R)
    (hA : A ∈ Metric.sphere O R)
    (hB : B ∈ Metric.sphere O R)
    (hC : C ∈ Metric.sphere O R)
    (hnBC_unit : ‖nBC‖ = 1)
    (hnBC_perp : inner (𝕜 := ℝ) (C -ᵥ B) nBC = 0)
    (hnBC_in : 0 < inner (𝕜 := ℝ) (A -ᵥ B) nBC)
    (hnCA_unit : ‖nCA‖ = 1)
    (hnCA_perp : inner (𝕜 := ℝ) (A -ᵥ C) nCA = 0)
    (hnCA_in : 0 < inner (𝕜 := ℝ) (B -ᵥ C) nCA)
    (hnAB_unit : ‖nAB‖ = 1)
    (hnAB_perp : inner (𝕜 := ℝ) (B -ᵥ A) nAB = 0)
    (hnAB_in : 0 < inner (𝕜 := ℝ) (C -ᵥ A) nAB)
    (hx : x = inner (𝕜 := ℝ) (O -ᵥ B) nBC)
    (hy : y = inner (𝕜 := ℝ) (O -ᵥ C) nCA)
    (hz : z = inner (𝕜 := ℝ) (O -ᵥ A) nAB)
    (hIr1 : inner (𝕜 := ℝ) (I -ᵥ B) nBC = r)
    (hIr2 : inner (𝕜 := ℝ) (I -ᵥ C) nCA = r)
    (hIr3 : inner (𝕜 := ℝ) (I -ᵥ A) nAB = r) :
    x + y + z = R + r

Sources

• https://en.wikipedia.org/wiki/Carnot%27s_theorem_(inradius,_circumradius). Statement ID: carnot-inradius-s1.

Used by 2

Used byJapanese theorem for concyclic quadrilaterals · Carnot's theorem (inradius and circumradius)

TheoremCarnot's theorem (inradius and circumradius)#✓fully proved

Let \(A, B, C\) be non-collinear points of a Euclidean affine plane lying on the circle with center \(O\) and radius \(R > 0\), and suppose \(O\) lies in the affine span of \(A, B, C\). Take unit vectors \(n_a\), \(n_b\), \(n_c\) normal to the sides and pointing toward the opposite vertices: \(n_a \perp C - B\) with \(\langle A - B, n_a \rangle > 0\), \(n_b \perp A - C\) with \(\langle B - C, n_b \rangle > 0\), and \(n_c \perp B - A\) with \(\langle C - A, n_c \rangle > 0\). Let \(x = \langle O - B, n_a \rangle\), \(y = \langle O - C, n_b \rangle\) and \(z = \langle O - A, n_c \rangle\) be the signed distances from \(O\) to the lines \(BC\), \(CA\), \(AB\). If a point \(I\) and a real number \(r > 0\) satisfy \(\langle I - B, n_a \rangle = \langle I - C, n_b \rangle = \langle I - A, n_c \rangle = r\) (so \(I\) is the incenter and \(r\) the inradius), then \(x + y + z = R + r\).

The hypotheses \(r > 0\) and that \(O\) lies in the affine span of \(A, B, C\) are not used; the general form of the theorem drops them.

MetaMathlibExt.carnot_inradius_circumradius · 30 lines

theorem carnot_inradius_circumradius
    {V : Type*} {P : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [MetricSpace P] [NormedAddTorsor V P]
    [Fact (Module.finrank ℝ V = 2)]
    (A B C O I : P) (R r x y z : ℝ)
    (nBC nCA nAB : V)
    (hTri : ¬ Collinear ℝ ({A, B, C} : Set P))
    (hRpos : 0 < R)
    (hOplane : O ∈ affineSpan ℝ {A, B, C})
    (hA : A ∈ Metric.sphere O R)
    (hB : B ∈ Metric.sphere O R)
    (hC : C ∈ Metric.sphere O R)
    (hnBC_unit : ‖nBC‖ = 1)
    (hnBC_perp : inner (𝕜 := ℝ) (C -ᵥ B) nBC = 0)
    (hnBC_in : 0 < inner (𝕜 := ℝ) (A -ᵥ B) nBC)
    (hnCA_unit : ‖nCA‖ = 1)
    (hnCA_perp : inner (𝕜 := ℝ) (A -ᵥ C) nCA = 0)
    (hnCA_in : 0 < inner (𝕜 := ℝ) (B -ᵥ C) nCA)
    (hnAB_unit : ‖nAB‖ = 1)
    (hnAB_perp : inner (𝕜 := ℝ) (B -ᵥ A) nAB = 0)
    (hnAB_in : 0 < inner (𝕜 := ℝ) (C -ᵥ A) nAB)
    (hx : x = inner (𝕜 := ℝ) (O -ᵥ B) nBC)
    (hy : y = inner (𝕜 := ℝ) (O -ᵥ C) nCA)
    (hz : z = inner (𝕜 := ℝ) (O -ᵥ A) nAB)
    (hrpos : 0 < r)
    (hIr1 : inner (𝕜 := ℝ) (I -ᵥ B) nBC = r)
    (hIr2 : inner (𝕜 := ℝ) (I -ᵥ C) nCA = r)
    (hIr3 : inner (𝕜 := ℝ) (I -ᵥ A) nAB = r) :
    x + y + z = R + r

Sources

• https://en.wikipedia.org/wiki/Carnot%27s_theorem_(inradius,_circumradius). Statement ID: carnot-inradius-s1.

Uses 1

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

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.