Fourier-Motzkin elimination of one variable

Let $A \in \mathbb{R}^{m \times (n+1)}$ and $c \in \mathbb{R}^m$, and write $\beta_i = A_{i,n}$ for the coefficient of the last variable in row $i$ and $\alpha_i \in \mathbb{R}^n$ for the remaining coefficients. Then the system $Ax \ge c$ in $n+1$ variables has a solution if and only if the following system in the $n$ unknowns $y$ has one:

This is one step of Fourier–Motzkin elimination. Necessity holds because each inequality of the reduced system is a nonnegative combination of two inequalities of the original one, chosen so that the last variable cancels: the pair inequality is $(-\beta_j)$ times row $i$ plus $\beta_i$ times row $j$. Sufficiency holds because a solution $y$ of the reduced system can be completed by any value $v$ of the last variable lying between the largest lower bound $\max_{\beta_i>0} (c_i - \alpha_i^{\mathsf T} y)/\beta_i$ and the smallest upper bound $\min_{\beta_j<0}(c_j - \alpha_j^{\mathsf T} y)/\beta_j$; the pair inequalities say precisely that every lower bound is at most every upper bound, and when one of the two families is empty any sufficiently extreme value works.

Iterating the step eliminates all variables and decides feasibility, which gives an elementary proof that linear feasibility over the reals is decidable, and, by tracking the nonnegative multipliers, the standard constructive route to Farkas' lemma and to linear programming duality. It also shows why the classical method is useless for the mission's goal: a single step can replace $m$ inequalities by roughly $m^2/4$, so eliminating $n$ variables in turn gives a bound that is doubly exponential in $n$, whereas Smale's ninth problem asks for a number of arithmetic operations polynomial in $m$ and $n$.