⊥ shortest — Perpendicular segment is shortest · Principia

Dependencies: perpendicular from a point (Perpendicular from a point to a line exists and is unique), Exterior angle > either non-adjacent interior angle (Exterior angle > either non-adjacent interior angle).

Statement

Let $P$ be a point not on a line $\ell$ . Drop a perpendicular from $P$ to $\ell$ with foot $F$ (existence and uniqueness guaranteed by perpendicular from a point). Then for any point $Q\neq F$ on $\ell$ ,

PF < PQ.

In other words: among all the segments from $P$ to points of $\ell$ , the perpendicular segment $PF$ is the shortest.

$Perpendicular segment is shortest schematic: P is off \ell, PF \perp \ell at F; for any Q\neq F on \ell, PF < PQ$

Proof

Examine the triangle $\triangle PFQ$ . Since $PF\perp\ell$ (by perpendicular from a point), $\angle PFQ = 90^\circ$ .

Apply Exterior angle > either non-adjacent interior angle to $\triangle PFQ$ : extending $\ell$ beyond $Q$ produces an exterior angle, and we conclude that $\angle PQF$ must be strictly less than the exterior angle of a non-adjacent interior angle, hence $\angle PQF < 90^\circ$ ; similarly $\angle FPQ < 90^\circ$ . Thus

\angle PFQ = 90^\circ\;>\;\angle PQF,\qquad \angle PFQ = 90^\circ\;>\;\angle FPQ.

$Step 1: \angle PFQ = 90^\circ (by perp-from-point) + exterior-angle inequality ⇒ \angle P, \angle Q < 90^\circ$

That is, $\angle F$ is the unique largest angle in $\triangle PFQ$ . By Bigger angle ↔ longer opposite side (the side opposite the largest angle is the longest), and since the side opposite $\angle F$ is $PQ$ , we have

PQ > PF. \qquad\blacksquare

$Step 2: \angle F = 90^\circ is the unique largest angle ⇒ by angle-side-inequality (larger angle opposite longer side), the opposite side PQ is the longest, hence PQ > PF$

Immediate consequences

Definition of "distance from a point to a line": from now on we can define "the distance from point $P$ to line $\ell$ " as $PF$ — this is the infimum of the distances from $P$ to the points of $\ell$ , and the infimum is attained (exactly when $Q=F$ ).
Unique minimum: $PQ$ , viewed as a function of the position of $Q$ on $\ell$ , is strictly monotonic on each of the two pieces split at $F$ — sliding $Q$ from $F$ to either side of $\ell$ strictly increases the distance. This simultaneously gives "the distance-minimizing point is unique".
Downstream applications: the standard proof of tangent ⊥ radius (Tangent is perpendicular to the radius at the point of tangency) uses this theorem: if a line through a point $T$ on a circle is not perpendicular to the radius $OT$ , then $O$ has a foot $F$ on that line with distance strictly less than $OT$ , so the line crosses into the interior of the circle — and therefore must meet the circle at a second point, hence is not a tangent.

Remarks

The final step in the proof — the longest side is opposite the largest angle — uses another independent middle-school geometry theorem Bigger angle ↔ longer opposite side ("Bigger angle ↔ longer opposite side"), which has not yet been written in Principia (planned for Wave 3a). For now, this entry simply invokes Bigger angle ↔ longer opposite side as a known fact; once Bigger angle ↔ longer opposite side is online, it should be added to this entry's meta.yaml.deps so the DAG verifier can complete this edge.

Apart from this last step, the entire proof uses only Perpendicular from a point to a line exists and is unique (guaranteeing $\angle F = 90^\circ$ ) and Exterior angle > either non-adjacent interior angle (guaranteeing the other two angles are strictly $< 90^\circ$ ); these two already pin down " $\angle F$ is the unique largest angle in $\triangle PFQ$ " completely. In other words, the geometric core of "the perpendicular segment is shortest" is the exterior-angle inequality — the size relations are all in place, all that remains is the final step of translating "angle size" back to "side length".