Show: "Checking no solution for system of linear equations with integer variables and coefficients" $\in \mathbf{NP}$ I've been struggling for a while trying to solve this problem:

Show that the following problem is in $\mathbf{NP}$:


  Check that a system of linear equations with $m$ integer variables and
  integer coefficients has no solution.




Let $L = \{\langle A, b \rangle\ |\ A \in \mathbb{Z}^m\times\mathbb{Z}^m\text{ and }Ax = b\text{ has no solution for }x \in \mathbb{Z}^{m} \}$

(please, feel free to correct if anywhere I'm wrong) 

For showing that a language is in $\mathbf{NP}$ we have to construct a Turing Machine, indicating what we have chosen as certificate. If the TM is nondeterministic, then nondeterministically we pick a certificate and check the condition. If it is deterministic, we pass the certificate as one of the parameters (of the two parameters TM. The other parameter is, in this case, the pair $\langle A, b \rangle$).

I'm having trouble trying to choose the appropriate certificate. 

My approaches:

1) Certificate: a vector $x \in \mathbb{Z}^{m}$, such that doesn't solve $Ax = b$. Issue: We would have to try every possible $x$ to show that $\nexists$ such vector for which solution may exist...

2) Certificate: Rank of $A$. if the $\mathrm{rank} A \neq m$, then the system has no solution and we $Accept$. Issue: doesn't necessarily mean that $x \in \mathbb{Z}^{m}$.

3) Consider $\overline{L} = \{\langle A, b \rangle\ |\ A \in \mathbb{Z}\times\mathbb{Z}\text{ and }Ax = b\text{ has a solution for }x \in \mathbb{Z}^{m} \}$.

Showing that the system has a solution seems easier than showing that there is no one. I guess the certificate has to be a vector $x \in \mathbb{Z}^{m}$, for which the $Ax = b$ is satisfied. Then, if I'm not mistaking, constructing a polynomial-time deterministic TM for $\overline{L}$ is straight forward. The thing is that this will show that $\overline{L} \in \mathbf{NP}$. This implies that $L \in$ co-$\mathbf{NP}$.

So showing that $L \in \mathbf{NP}$ would be equivalent to showing that co-$\mathbf{NP} = \mathbf{NP}$??
There is a polynomial time algorithm that determines whether a system of linear equations over the integers has a solution. The algorithm uses Hermite normal form, which can be computed in polynomial time. See lecture notes of Swastik Kopparty: Hermite normal form and finding integer solutions.

Your proof that your problem is in coNP is incomplete, since you haven't shown that the witness has polynomial size. Assuming you did manage to show it, all this implies is that the problem is in coNP, not that it is coNP-hard. There's absolutely no issue for a problem to be in both NP and coNP. Indeed, every problem in P is also in NP and coNP. If you can put a problem in both NP and coNP, then this suggests that it might actually be in P, though it is conjectured that $\mathsf{P} \subsetneq \mathsf{NP} \cap \mathsf{coNP}$. One problem which might lie in the middle is (a decision version of) integer factorization.