Farkas' lemma: exactly one of Ax = b, x ≥ 0 and Aᵀp ≥ 0, pᵀb < 0 is solvable

Farkas' lemma. Let $A \in \mathbb{R}^{m \times n}$ and $b \in \mathbb{R}^m$. Exactly one of the following two systems is solvable:

Equivalently, $b$ lies in the cone generated by the columns of $A$ precisely when every vector $p$ having nonnegative inner product with each column also has nonnegative inner product with $b$.

This transposition theorem is the algebraic core of linear programming: duality, the optimality conditions for a linear program in standard form, and the description of the normal cone of $\{x : Ax=b,\ x \ge 0\}$ all follow from it. It is Theorem 4.6 (p. 165) of Bertsimas & Tsitsiklis, Introduction to Linear Optimization.

Formalization note. Xor is exclusive disjunction, so the statement asserts both that the alternatives are incompatible and that one of them holds. Vectors are functions out of Fin n, and 0 ≤ x is the pointwise order. The statement is the finitely generated (column) form of Farkas' lemma; it is not a specialization of the Hilbert-space separation theorem for closed convex cones, because closedness of the column cone is part of what has to be established.