We show that a linear matrix inequality is feasible if and only if the natural quadratic module associated to it is proper. This quadratic module consists of all polynomials possessing a natural sums of squares certificate for being nonnegative on the spectrahedron defined by the linear matrix inequality. We interpret this as a natural version of Farkas' lemma working for semidefinite programming.