垂线段最短 — 垂线段最短 · Principia

依赖：过点作垂线（过一点作已知直线的垂线 · 存在且唯一）、三角形外角大于任一不相邻内角（三角形外角大于任一不相邻内角）。

陈述

设直线 $\ell$ 外有一点 $P$ 。从 $P$ 向 $\ell$ 作垂线，垂足为 $F$ （过点作垂线 保证存在且唯一）。则对 $\ell$ 上任意一点 $Q\neq F$ ，都有

PF < PQ.

也就是说：从 $P$ 到 $\ell$ 上各点的所有线段里，垂线段 $PF$ 是最短的那一条。

$垂线段最短示意：P 在 \ell 外，PF \perp \ell 于 F；对 \ell 上任意 Q\neq F 都有 PF < PQ$

证明

考察三角形 $\triangle PFQ$ 。由 $PF\perp\ell$ （过点作垂线）， $\angle PFQ = 90^\circ$ 。

对 $\triangle PFQ$ 应用三角形外角大于任一不相邻内角：在 $\ell$ 上把 $Q$ 端延长成外角，可知 $\angle PQF$ 必定严格小于与之不相邻的某一内角的"外角"，从而 $\angle PQF < 90^\circ$ ；同理 $\angle FPQ < 90^\circ$ 。于是

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

$Step 1：\angle PFQ = 90^\circ（由 perp-from-point）+ 外角不等式 ⇒ \angle P, \angle Q < 90^\circ$

也就是说 $\angle F$ 是 $\triangle PFQ$ 中唯一的最大角。大角对大边：最大角所对的边最长，而 $\angle F$ 所对的边正是 $PQ$ ，所以

PQ > PF. \qquad\blacksquare

$Step 2：\angle F = 90^\circ 是唯一最大角 ⇒ 由 angle-side-inequality（大角对大边），所对的 PQ 是最长边，故 PQ > PF$

即时推论

"点到直线的距离"的定义：从此可以把"点 $P$ 到直线 $\ell$ 的距离"定义为 $PF$ —— 这是 $P$ 到 $\ell$ 上一切点的距离的下确界，且这下确界可达（恰好在 $Q=F$ 时达到）。
唯一极小： $PQ$ 关于 $Q$ 在 $\ell$ 上的位置是严格单调的两段——从 $F$ 出发向 $\ell$ 的两侧任意滑动，距离都严格增加。这同时给出"距离极小点唯一"。
下游应用：切线 ⊥ 半径（切线垂直于过切点的半径）的标准证法即用本定理：若过圆上一点 $T$ 的直线与半径 $OT$ 不垂直，则 $O$ 到该直线上必有距离严格小于 $OT$ 的脚点 $F$ ，于是该直线在圆内部穿过——它必然与圆有第二交点，从而不是切线。

备注

证明的最后一步——最大角对最长边——所用的事实是另一条独立的初中几何定理大角对大边（"大角对大边"），目前在 Principia 里尚未编写（计划在 Wave 3a 完成）。本条目暂以大角对大边作为已知事实直接调用；待大角对大边上线后，应将其加入本词条 meta.yaml.deps，由 DAG 验证补全这一条边。

除最后这一步以外，整个证明只用到了过一点作已知直线的垂线 · 存在且唯一（保证 $\angle F = 90^\circ$ ）与三角形外角大于任一不相邻内角（保证另两角严格 $< 90^\circ$ ）；这两条已经把" $\angle F$ 是 $\triangle PFQ$ 中唯一的最大角"完全锁死。换句话说，"垂线段最短"的几何内核是外角不等式——大小关系都已就位，只差最后一步把"角的大小"翻译回"边的长短"。