Perpendicular segment is shortest

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$,

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